/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30/FONT#10=ZERO30/FONT#11=BAXI30/FONT#10=ZERO30
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ H


␈↓ ↓H␈↓α␈↓ α$REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC

␈↓ ↓H␈↓α␈↓ ¬Jby John McCarthy











␈↓ ↓H␈↓␈↓ α_This␈αpaper␈αpresents␈αmethods␈αof␈αrepresenting␈αrecursive␈αprograms␈αby␈αsentences␈αand␈αschemata
␈↓ ↓H␈↓of␈α
first␈α
order␈α
logic,␈α
characterization␈α
of␈α
␈↓↓recursion␈α
induction␈↓,␈α
␈↓↓subgoal␈α
induction␈↓,␈α∞␈↓↓inductive␈α
assertions␈↓
␈↓ ↓H␈↓and␈α⊂other␈α⊂ways␈α⊂of␈α⊂proving␈α⊂facts␈α⊂about␈α⊂programs␈α⊂as␈α⊂axiom␈α⊂schemata␈α⊂of␈α⊂first␈α⊂order␈α⊂logic,␈α∂and
␈↓ ↓H␈↓applications of these results to proving assertions about programs.

␈↓ ↓H␈↓␈↓εThis draft of FIRST.NEW[W77,JMC] PUBbed at 9:01 on March 14, 1978.␈↓
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 91


␈↓ ↓H␈↓α1. Introduction and Motivation.

␈↓ ↓H␈↓␈↓ α_It␈α
has␈αbeen␈α
concluded␈αfrom␈α
the␈α
undecideability␈αof␈α
both␈αequivalence␈α
and␈αnon-equivalence␈α
of
␈↓ ↓H␈↓abstract␈α⊃recursive␈α⊃program␈α⊃schemata␈α⊃that␈α⊃recursive␈α⊃programs␈α⊃cannot␈α⊃be␈α⊃characterized␈α⊃in␈α⊂first
␈↓ ↓H␈↓order␈α⊂logic.␈α⊃ Cooper␈α⊂(1969)␈α⊂showed␈α⊃how␈α⊂to␈α⊂characterize␈α⊃them␈α⊂in␈α⊂second␈α⊃order␈α⊂logic,␈α⊃and␈α⊂that
␈↓ ↓H␈↓seemed␈α∪to␈α∩settle␈α∪the␈α∪matter.␈α∩ However,␈α∪we␈α∩will␈α∪exhibit␈α∪first␈α∩order␈α∪characterizations␈α∪that␈α∩are
␈↓ ↓H␈↓incomplete␈α∞only␈α∞in␈α∞that␈α∞they␈α∞admit␈α∞non-standard␈α∞models␈α∞like␈α∞those␈α∞of␈α∞first␈α∞order␈α∞arithmetic.␈α
 It
␈↓ ↓H␈↓now␈α∂seems␈α∂likely␈α∂that␈α⊂all␈α∂"ordinary"␈α∂␈↓↓extensional␈↓␈α∂assertions␈α⊂about␈α∂programs␈α∂will␈α∂be␈α⊂provable␈α∂or
␈↓ ↓H␈↓disprovable␈αin␈αfirst␈αorder␈αtheories.␈α ␈↓↓Extensional␈↓␈αassertions␈αabout␈αa␈αprogram␈αconcern␈αthe␈αfunctions
␈↓ ↓H␈↓computed␈αby␈αthe␈αprogram␈αand␈αnot␈αthe␈αmanner␈αof␈αcomputation.␈α That␈αa␈αmerge␈αsort␈αprogram␈αgives
␈↓ ↓H␈↓the␈αsame␈αresult␈αas␈αa␈αbubble␈αsort␈αprogram␈αis␈αan␈αextensional␈αassertion,␈αbut␈αthe␈αfact␈αthat␈αit␈αdoes␈αless
␈↓ ↓H␈↓computation is not.

␈↓ ↓H␈↓␈↓ α_Besides␈αilluminating␈αthe␈αlogical␈αstructure␈αof␈αcomputer␈αprograms,␈αthese␈αresults␈αhave␈αpractical
␈↓ ↓H␈↓significance.␈α∪ First,␈α∀the␈α∪correctness␈α∪of␈α∀a␈α∪computer␈α∪program␈α∀often␈α∪involves␈α∪facts␈α∀about␈α∪other
␈↓ ↓H␈↓mathematical␈αdomains,␈α
and␈αthese␈αare␈α
often␈αconveniently␈αexpressed␈α
in␈αfirst␈αorder␈α
logic␈αor␈αin␈α
a␈αset
␈↓ ↓H␈↓theory␈αaxiomatized␈α
in␈αfirst␈α
order␈αlogic.␈α
 It␈αhas␈αproved␈α
particularly␈αdifficult␈α
to␈αwork␈α
within␈αlogics
␈↓ ↓H␈↓that␈α∃admit␈α∀only␈α∃continuous␈α∀functions␈α∃and␈α∀predicates.␈α∃ Second,␈α∀proof-checking␈α∃and␈α∀theorem
␈↓ ↓H␈↓proving␈αprograms␈αhave␈αbeen␈αdeveloped␈αfor␈αfirst␈αorder␈αlogic.␈α Finally,␈αfirst␈αorder␈αlogic␈αis␈αcomplete,
␈↓ ↓H␈↓so␈α∞that␈α∞the␈α∂G␈↓
:␈↓odelian␈α∞incompleteness␈α∞of␈α∂any␈α∞theory␈α∞is␈α∞in␈α∂the␈α∞set␈α∞of␈α∂axioms␈α∞and␈α∞can␈α∂be␈α∞reduced
␈↓ ↓H␈↓when necessary by adding axioms rather than by changing the logical system.

␈↓ ↓H␈↓␈↓ α_While␈α↔our␈α↔goal␈α↔is␈α⊗first␈α↔order␈α↔representations␈α↔of␈α⊗recursive␈α↔programs,␈α↔we␈α↔will␈α⊗make
␈↓ ↓H␈↓considerable informal use of higher order functionals and predicates.

␈↓ ↓H␈↓␈↓ α_We␈α⊗present␈α↔two␈α⊗methods␈α↔of␈α⊗representing␈α↔recursive␈α⊗programs.␈α↔ The␈α⊗first␈α↔involves␈α⊗a
␈↓ ↓H␈↓␈↓↓functional␈α∞equation␈↓␈α∞and␈α∞a␈α∞␈↓↓minimization␈α∞schema␈↓␈α∞for␈α∞each␈α∞program.␈α∞ The␈α∞functional␈α∞equation␈α∞has
␈↓ ↓H␈↓the␈αfunction␈αon␈αboth␈αsides␈αof␈αan␈αequality␈αsign␈αand␈αso␈αdefines␈αit␈αimplicitly.␈α However,␈αall␈αvariables
␈↓ ↓H␈↓are␈α∞universally␈α∞quantified.␈α∞ The␈α∞second␈α∂approach␈α∞defines␈α∞the␈α∞function␈α∞explicitly,␈α∂but␈α∞existential
␈↓ ↓H␈↓quantifiers␈α
asserting␈α
the␈αexistence␈α
of␈α
finite␈αapproximations␈α
to␈α
the␈αfunction␈α
occur␈α
in␈α
the␈αformula.
␈↓ ↓H␈↓The␈α
fact␈α
that␈α
the␈α
functional␈α
equation␈α
of␈α
a␈α
program␈α
not␈α
known␈α
to␈α
terminate␈α
can␈α
nevertheless␈αbe
␈↓ ↓H␈↓written so simply in first order logic was discovered by Cartwright (1977), but the rest seems new.


␈↓ ↓H␈↓α2. Recursive Programs.

␈↓ ↓H␈↓␈↓ α_An␈α
adequate␈α
background␈α
for␈α
this␈α
paper␈α
is␈α
contained␈α
in␈α
(Manna␈α
1974)␈α
and␈α
more␈α
concisely␈α
in
␈↓ ↓H␈↓(Manna,␈α∂Ness␈α∞and␈α∂Vuillemin␈α∞1973).␈α∂ The␈α∞connections␈α∂of␈α∞recursive␈α∂programs␈α∞with␈α∂second␈α∞order
␈↓ ↓H␈↓logic are given in (Cooper 1969) and (Park 1970).

␈↓ ↓H␈↓␈↓ α_We consider ␈↓↓recursive programs␈↓ of the form

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓f(x) ← ␈↓	t␈↓↓[f](x)␈↓,

␈↓ ↓H␈↓where ␈↓	t␈↓ is a ␈↓↓computable functional␈↓ like

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓␈↓	t␈↓↓ = λf.λx.(␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ x . f(x - 1))␈↓,

␈↓ ↓H␈↓which gives rise to the well known recursive definition of the factorial function, namely
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 92


␈↓ ↓H␈↓3)␈↓ α8  ␈↓↓n! ← ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ n . (n - 1)!␈↓.

␈↓ ↓H␈↓␈↓ α_In␈α
general,␈α
we␈α
shall␈α
be␈αinterested␈α
in␈α
partial␈α
functions␈α
from␈αa␈α
domain␈α
D1␈α
to␈α
a␈α
domain␈αD2.
␈↓ ↓H␈↓We␈α⊃augment␈α⊂these␈α⊃domains␈α⊃by␈α⊂an␈α⊃undefined␈α⊃element␈α⊂called␈α⊃␈↓πT␈↓␈α⊃(read␈α⊂"bottom")␈α⊃giving␈α⊃rise␈α⊂to
␈↓ ↓H␈↓domains␈αD1␈↓∧+␈↓␈αand␈αD2␈↓∧+␈↓.␈α A␈αset␈α␈↓↓F␈↓␈αof␈αtotal␈αbase␈αfunctions␈αon␈αthe␈αdomains␈αis␈αassumed␈αavailable,␈αand
␈↓ ↓H␈↓we study functions ␈↓↓computable from the set F␈↓ as in (McCarthy 1963).

␈↓ ↓H␈↓␈↓ α_It␈αis␈αnecessary␈αto␈αdistinguish␈αbetween␈αa␈αprogram␈αas␈αa␈αtext␈αand␈αthe␈αpartial␈α
function␈αdefined
␈↓ ↓H␈↓by␈α⊃the␈α⊃program␈α⊂when␈α⊃one␈α⊃is␈α⊂interested␈α⊃in␈α⊃describing␈α⊂the␈α⊃dependence␈α⊃of␈α⊂the␈α⊃function␈α⊃on␈α⊂the
␈↓ ↓H␈↓interpretation␈α
of␈α
the␈α
basic␈αfunction␈α
and␈α
predicate␈α
symbols.␈α
 However,␈αwe␈α
will␈α
be␈α
working␈αwith␈α
just
␈↓ ↓H␈↓one␈α
interpretation␈α
at␈αa␈α
time,␈α
so␈αwe␈α
won't␈α
use␈αseparate␈α
symbols␈α
for␈αprograms␈α
and␈α
the␈αfunctions␈α
they
␈↓ ↓H␈↓determine.


␈↓ ↓H␈↓α3. The Functional Equation of a Recursive Program.

␈↓ ↓H␈↓␈↓ α_Consider the Lisp program

␈↓ ↓H␈↓4)␈↓ α8  ␈↓↓subst[x,y,z] ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ z ␈↓αthen␈↓↓ [␈↓αif␈↓↓ z=y ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ z] ␈↓αelse␈↓↓ subst[x,y,␈↓αa␈↓↓ z] . subst[x,y,␈↓αd␈↓↓ z]␈↓.

␈↓ ↓H␈↓The␈α
above␈α
is␈α
in␈α
Lisp␈α
␈↓↓external␈↓␈α
or␈α
␈↓↓publication␈↓␈α
notation␈α
in␈α
which␈α
 ␈↓αa␈↓ ␈↓↓x␈↓ ␈α
(bold␈α
face␈α
␈↓αa␈↓)␈α
stands␈α
for␈α
␈↓↓car[x]␈↓,
␈↓ ↓H␈↓ ␈↓αd␈↓ ␈↓↓x␈↓ ␈α∂for␈α∂␈↓↓cdr[x]␈↓,␈α⊂ ␈↓↓x . y␈↓ ␈α∂for␈α∂␈↓↓cons[x,y]␈↓,␈α∂ ␈↓αat␈↓ ␈↓↓x␈↓ ␈α⊂for␈α∂␈↓↓atom[x]␈↓,␈α∂ ␈↓αn␈↓ ␈↓↓x␈↓ ␈α∂for␈α⊂␈↓↓null[x]␈↓,␈α∂and␈α∂␈↓↓<x␈↓β1␈↓↓␈α∂...␈α⊂x␈↓βn␈↓>␈α∂for
␈↓ ↓H␈↓␈↓↓list[x␈↓β1␈↓↓,␈α
...␈α
,x␈↓βn␈↓],␈α
and␈α
␈↓↓x * y␈↓␈α
for␈α
␈↓↓append[x,y]␈↓.␈α
 Equality␈α
is␈α
taken␈α
as␈α
equality␈α
of␈α
S-expressions␈αso␈α
that
␈↓ ↓H␈↓␈↓αeq␈↓ is not used.  The program is written

␈↓ ↓H␈↓␈↓ α_(DE␈αSUBST␈α(X␈αY␈αZ)␈α(COND␈α((ATOM␈αZ)␈α(COND␈α((EQUAL␈αZ␈αY)␈αX)␈α(T␈αZ)))␈α(T␈α(CONS
␈↓ ↓H␈↓(SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))

␈↓ ↓H␈↓in Lisp ␈↓↓internal notation␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α∞basic␈α
functions␈α∞{␈↓↓car,␈α
cdr,␈α∞cons,␈α
atom}␈↓␈α∞of␈α∞Lisp␈α
are␈α∞all␈α
assumed␈α∞total,␈α
but␈α∞we␈α∞will␈α
say
␈↓ ↓H␈↓nothing␈α∞about␈α∞the␈α∞values␈α∞of␈α∞␈↓↓car␈↓␈α∞and␈α∞␈↓↓cdr␈↓␈α∞when␈α∞applied␈α∞to␈α∞atoms.␈α∞ According␈α∞to␈α∞the␈α∞fixed␈α∞point
␈↓ ↓H␈↓theory␈α∞of␈α∞recursive␈α∞programs,␈α∞any␈α∂such␈α∞program␈α∞defines␈α∞a␈α∞function␈α∂␈↓↓f␈↓␈α∞from␈α∞␈↓↓Sexp␈↓␈α∞(the␈α∞set␈α∂of␈α∞S-
␈↓ ↓H␈↓expressions)␈αto␈αSexp␈↓∧+␈↓␈α(the␈αset␈αof␈αS-expressions␈αaugmented␈αby␈α␈↓πT␈↓).␈α This␈αfunction␈αcan␈αbe␈αcomputed
␈↓ ↓H␈↓by␈α∂any␈α∂␈↓↓safe␈α∞computation␈α∂rule␈↓,␈α∂(in␈α∂the␈α∞terminology␈α∂of␈α∂Manna,␈α∞Ness,␈α∂and␈α∂Vuillemin␈α∂(1973)),␈α∞and
␈↓ ↓H␈↓when␈α
the␈α
computation␈α
terminates,␈α
its␈α
value␈α
will␈α
belong␈α
to␈α
␈↓↓Sexp.␈↓␈α
 When␈α
the␈α
computation␈αdoesn't
␈↓ ↓H␈↓terminate,␈α∂we␈α∂postulate␈α∞␈↓↓f(x) = ␈↓πT␈↓↓␈↓.␈α∂ Although␈α∂the␈α∂particular␈α∞function␈α∂␈↓↓subst␈↓␈α∂always␈α∂terminates,␈α∞our
␈↓ ↓H␈↓first␈α∂order␈α∞formula␈α∂doesn't␈α∞assume␈α∂it.␈α∞ Instead,␈α∂the␈α∞first␈α∂order␈α∞formula␈α∂(5)␈α∞below␈α∂is␈α∂the␈α∞starting
␈↓ ↓H␈↓point of a structural induction proof that ␈↓↓subst␈↓ is total.

␈↓ ↓H␈↓␈↓ α_These facts show that the function ␈↓↓subst␈↓ defined recursively by (4) satisfies the sentence

␈↓ ↓H␈↓5)␈↓ α8␈α⊃ ␈↓↓∀x␈α⊃y␈α⊃z.(subst(x,y,z)␈α⊃=␈α⊂␈↓αif␈↓↓␈α⊃␈↓αat␈↓↓␈α⊃z␈α⊃␈↓αthen␈↓↓␈α⊃(␈↓αif␈↓↓␈α⊂z␈α⊃=␈α⊃y␈α⊃␈↓αthen␈↓↓␈α⊃x␈α⊂␈↓αelse␈↓↓␈α⊃z)␈α⊃␈↓αelse␈↓↓␈α⊃subst(x,y,␈↓αa␈↓↓␈α⊃z)␈α⊂.
␈↓ ↓H␈↓↓subst(x,y,␈↓αd␈↓↓ z))␈↓

␈↓ ↓H␈↓of␈α
first␈αorder␈α
logic.␈α
 The␈αvariables␈α
␈↓↓x,␈αy␈↓␈α
and␈α
␈↓↓z␈↓␈αrange␈α
over␈α␈↓↓Sexp;␈↓␈α
when␈α
we␈αwant␈α
to␈α
quantify␈αover
␈↓ ↓H␈↓␈↓↓Sexp␈↓∧+␈↓,␈α⊃we␈α⊃use␈α⊂␈↓↓X,␈α⊃Y␈α⊃␈↓and␈↓↓␈α⊂Z␈↓.␈α⊃ Moreover,␈α⊃we␈α⊂are␈α⊃augmenting␈α⊃first␈α⊂order␈α⊃logic,␈α⊃as␈α⊃described␈α⊂in
␈↓ ↓H␈↓(Manna␈α1974),␈α
by␈αallowing␈αconditional␈α
expressions␈αas␈αterms.␈α
 The␈αaugmentation␈αdoes␈α
not␈αchange
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 93


␈↓ ↓H␈↓what␈α∀can␈α∀be␈α∀expressed␈α∀in␈α∀first␈α∃order␈α∀logic,␈α∀because␈α∀conditional␈α∀expressions␈α∀can␈α∃always␈α∀be
␈↓ ↓H␈↓eliminated from sentences by distributing predicates over them.  Thus (5) can be written

␈↓ ↓H␈↓6)␈↓ α8␈α ␈↓↓∀x␈αy␈αz.(␈↓αat␈↓↓␈αz␈α⊃␈α(z=y␈α⊃␈αsubst(x,y,z)␈α=␈αx)␈α∧␈αz≠y␈α⊃␈αsubst(x,y,z)␈α=␈αz)␈α∧␈α¬␈↓αat␈↓↓␈αz␈α⊃␈αsubst(x,y,z)
␈↓ ↓H␈↓↓= subst(x,y,␈↓αa␈↓↓ z) . subst(x,y,␈↓αd␈↓↓ z)),␈↓

␈↓ ↓H␈↓but␈α∪we␈α∪will␈α∪use␈α∪conditional␈α∪expressions,␈α∩because␈α∪they␈α∪are␈α∪clearer␈α∪and␈α∪express␈α∪the␈α∩recursive
␈↓ ↓H␈↓program␈αdirectly.␈α
 Indeed,␈αwe␈α
recommend␈αtheir␈αuse␈α
as␈αterms␈α
in␈αlogic␈αgenerally,␈α
and␈αin␈α
first␈αorder
␈↓ ↓H␈↓logic␈α∩in␈α∩particular.␈α⊃ They␈α∩don't␈α∩extend␈α∩the␈α⊃logical␈α∩power,␈α∩but␈α∩they␈α⊃permit␈α∩many␈α∩facts␈α∩to␈α⊃be
␈↓ ↓H␈↓expressed without circumlocution.

␈↓ ↓H␈↓␈↓ α_One␈αgoal␈αof␈α
our␈αfirst␈αorder␈α
representation␈αis␈αto␈αuse␈α
(4)␈αonly␈αto␈α
justify␈αwriting␈α(5)␈α
and␈αthen
␈↓ ↓H␈↓prove all properties of ␈↓↓subst␈↓ using a first order axiomatization of Lisp.




␈↓ ↓H␈↓α4. First Order Axioms for Lisp.

␈↓ ↓H␈↓␈↓ α_We␈α⊂use␈α⊃lower␈α⊂case␈α⊂variables␈α⊃␈↓↓x,␈↓␈α⊂␈↓↓y,␈↓␈α⊃and␈α⊂␈↓↓z␈↓␈α⊂with␈α⊃or␈α⊂without␈α⊂subscripts␈α⊃to␈α⊂range␈α⊃over␈α⊂S-
␈↓ ↓H␈↓expressions.␈α Capitalized␈αvariables␈αrange␈αover␈αall␈αentities.␈α
 We␈αalso␈αuse␈αvariables␈α␈↓↓u,␈↓␈α␈↓↓v␈↓␈αand␈α␈↓↓w␈↓␈α
with
␈↓ ↓H␈↓or␈α∂without␈α∂subscripts␈α∂to␈α∂range␈α∂over␈α∂lists,␈α∂i.e.␈α∂S-expressions␈α∂such␈α∂that␈α∂successive␈α∂␈↓↓cdr␈↓s␈α∂eventually
␈↓ ↓H␈↓reach␈αNIL.␈α (The␈α␈↓↓car␈↓␈αof␈αa␈αlist␈αis␈αnot␈αrequired␈αto␈αbe␈αa␈αlist).␈α We␈αuse␈αpredicates␈α␈↓↓issexp␈↓␈αand␈α␈↓↓islist␈↓␈αto
␈↓ ↓H␈↓assert␈α∪that␈α∪an␈α∀individual␈α∪is␈α∪an␈α∀S-expression␈α∪or␈α∪a␈α∪list.␈α∀ First␈α∪come␈α∪the␈α∀"housekeeping"␈α∪and
␈↓ ↓H␈↓"algebraic" axioms:

␈↓ ↓H␈↓L1:     ␈↓↓∀x.issexp x␈↓

␈↓ ↓H␈↓L2:     ␈↓↓∀u.islist u␈↓

␈↓ ↓H␈↓L3:     ␈↓↓∀u.issexp u␈↓

␈↓ ↓H␈↓L4:     ␈↓↓¬issexp ␈↓πT␈↓↓

␈↓ ↓H␈↓↓L5:     islist ␈↓NIL

␈↓ ↓H␈↓L6:     ␈↓↓␈↓αat␈↓↓ ␈↓NIL␈↓↓␈↓

␈↓ ↓H␈↓L7:     ␈↓↓∀u.(␈↓αat␈↓↓ u ⊃ u = ␈↓NIL␈↓↓)␈↓

␈↓ ↓H␈↓L8:     ␈↓↓∀x y.issexp (x.y)␈↓

␈↓ ↓H␈↓L9:     ␈↓↓∀x u.islist (x.u)␈↓

␈↓ ↓H␈↓L10:    ␈↓↓∀x. ¬␈↓αat␈↓↓ x ⊃ issexp ␈↓αa␈↓↓ x␈↓

␈↓ ↓H␈↓L11:    ␈↓↓∀x. ¬␈↓αat␈↓↓ x ⊃ issexp ␈↓αd␈↓↓ x␈↓

␈↓ ↓H␈↓L12:    ␈↓↓∀u. u ≠ ␈↓NIL␈↓↓ ⊃ islist ␈↓αd␈↓↓ u␈↓
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 94


␈↓ ↓H␈↓L13:    ␈↓↓∀x y. ␈↓αa␈↓↓ (x.y) = x␈↓

␈↓ ↓H␈↓L14:    ␈↓↓∀x y. ␈↓αd␈↓↓ (x.y) = y␈↓

␈↓ ↓H␈↓L15:    ␈↓↓∀x y. ¬␈↓αat␈↓↓ (x.y)␈↓

␈↓ ↓H␈↓L16:    ␈↓↓∀x.¬␈↓αat␈↓↓ x ⊃ (␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x) = x␈↓

␈↓ ↓H␈↓␈↓ α_Next we have axiom schemata of induction

␈↓ ↓H␈↓LS1:    ␈↓↓(∀x.␈↓αat␈↓↓ x ⊃ ␈↓	F␈↓↓ x) ∧ ∀x.(¬␈↓αat␈↓↓ x ∧ ␈↓	F␈↓↓ ␈↓αa␈↓↓ x ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ x ⊃ ␈↓	F␈↓↓ x) ⊃ ∀x.␈↓	F␈↓↓ x␈↓

␈↓ ↓H␈↓LS2:    ␈↓↓(∀u.u = ␈↓NIL␈↓↓ ⊃ ␈↓	F␈↓↓ u) ∧ ∀u.(u ≠ ␈↓NIL␈↓↓ ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ u ⊃ ␈↓	F␈↓↓ u) ⊃ ∀u. ␈↓	F␈↓↓ u␈↓.

␈↓ ↓H␈↓␈↓ α_From these axioms and schemata, we can prove

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓∀x y z.issexp subst(x,y,z)␈↓

␈↓ ↓H␈↓which␈α
is␈α
our␈α
way␈α
of␈α
saying␈αthat␈α
␈↓↓subst␈↓␈α
is␈α
total.␈α
 The␈α
key␈αstep␈α
is␈α
applying␈α
the␈α
axiom␈α
schema␈αLS1
␈↓ ↓H␈↓with␈α∩the␈α∩predicate␈α∪␈↓↓␈↓	F␈↓↓(z)␈α∩≡␈α∩issexp␈α∩subst(x,y,z)␈↓.␈α∪ We␈α∩can␈α∩also␈α∩prove␈α∪in␈α∩first␈α∩order␈α∪logic␈α∩such
␈↓ ↓H␈↓algebraic properties of ␈↓↓subst␈↓ as

␈↓ ↓H␈↓8)␈↓ α8  ␈↓↓∀x y z y1 z1.(¬occur(y,z1) ⊃ subst(subst(x,y,z),y1,z1) = subst(x,y,subst(z,y1,z1)))␈↓

␈↓ ↓H␈↓if␈αwe␈αhave␈αsuitable␈αaxiomatization␈αof␈αthe␈αpredicate␈α␈↓↓occur(x,y)␈↓␈αmeaning␈αthat␈αthe␈αatom␈α␈↓↓x␈↓␈αoccurs␈αin
␈↓ ↓H␈↓the S-expression ␈↓↓y.␈↓

␈↓ ↓H␈↓␈↓ α_The␈α
axiomatization␈α
of␈α
the␈α
predicate␈α
␈↓↓occur␈↓␈α
raises␈α
some␈α
new␈α
problems.␈α
 It␈α
is␈α
defined␈α∞by␈α
the
␈↓ ↓H␈↓recursive Lisp program

␈↓ ↓H␈↓9)␈↓ α8  ␈↓↓occur(x,y) ← (x = y) ∨ (¬␈↓αat␈↓↓ y ∧ (occur(x,␈↓αa␈↓↓ y) ∨ occur(x,␈↓αd␈↓↓ y)))␈↓.

␈↓ ↓H␈↓If␈α∂we␈α∂were␈α∂sure␈α∂in␈α∞advance␈α∂that␈α∂␈↓↓occur␈↓␈α∂were␈α∂total,␈α∂we␈α∞could␈α∂translate␈α∂the␈α∂recursion␈α∂(9)␈α∂into␈α∞the
␈↓ ↓H␈↓sentence

␈↓ ↓H␈↓10)␈↓ α8  ␈↓↓∀x y.(occur(x,y) ≡ (x = y) ∨ (¬␈↓αat␈↓↓ y ∧ (occur(x,␈↓αa␈↓↓ y) ∨ occur(x,␈↓αd␈↓↓ y))))␈↓

␈↓ ↓H␈↓which␈α⊂will␈α∂suffice␈α⊂for␈α∂proving␈α⊂(8),␈α∂but␈α⊂we␈α∂have␈α⊂no␈α∂right␈α⊂to␈α∂write␈α⊂it␈α∂down␈α⊂from␈α⊂the␈α∂recursive
␈↓ ↓H␈↓definition (9).

␈↓ ↓H␈↓␈↓ α_What we may write without proving that ␈↓↓occur␈↓ is total is an implicit definition

␈↓ ↓H␈↓11)␈↓ α8  ␈↓↓∀x y.(occura(x,y) = (x equals y) or (not atom y and (occura(x,␈↓αa␈↓↓ y) or occura(x,␈↓αd␈↓↓ y))))␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓12)␈↓ α8  ␈↓↓∀x y.(occur(x,y) ≡ (occura(x,y) = T))␈↓.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 95


␈↓ ↓H␈↓From␈α∞(11),␈α∞we␈α∞can␈α∞prove␈α∞that␈α∞␈↓↓occura␈↓␈α∂is␈α∞total␈α∞by␈α∞structural␈α∞induction␈α∞and␈α∞from␈α∞this␈α∂(10)␈α∞quickly
␈↓ ↓H␈↓follows.

␈↓ ↓H␈↓␈↓ α_Since␈αrecursive␈αdefinitions␈αgive␈αrise␈αto␈αpartial␈α
predicates,␈αand␈αwe␈αdon't␈αwant␈αto␈αuse␈αa␈α
partial
␈↓ ↓H␈↓predicate␈α∞logic,␈α∞we␈α∞introduce␈α∂a␈α∞domain␈α∞␈↓	P␈↓␈α∞of␈α∂␈↓↓extended␈α∞truth␈α∞values␈↓␈α∞with␈α∂characteristic␈α∞predicate
␈↓ ↓H␈↓␈↓↓isetv␈↓␈α
whose␈α
elements␈α
are␈α∞␈↓↓T,␈↓␈α
␈↓↓F␈↓␈α
and␈α
␈↓πT␈↓.␈α∞ There␈α
is␈α
no␈α
harm␈α
in␈α∞identifying␈α
␈↓↓T␈↓␈α
and␈α
␈↓↓F␈↓␈α∞with␈α
suitable
␈↓ ↓H␈↓Lisp␈αatoms␈αor␈αwith␈αthe␈αintegers␈α1␈αand␈α0.␈α The␈αfollowing␈αaxioms␈αdescribe␈αfunctions␈αinto␈αor␈αout␈αof
␈↓ ↓H␈↓␈↓	P␈↓.  We use the predicate ␈↓↓istv␈↓ to test for the honest truth values ␈↓↓T␈↓ and ␈↓↓F.␈↓

␈↓ ↓H␈↓B1:     ␈↓↓∀p.(isetv p)␈↓

␈↓ ↓H␈↓B2:     ␈↓↓∀p.(p = T ∨ p = F ∨ p = ␈↓πT␈↓↓)␈↓

␈↓ ↓H␈↓B3:     ␈↓↓T ≠ F ∧ T ≠ ␈↓πT␈↓↓ ∧ F ≠ ␈↓πT␈↓↓␈↓

␈↓ ↓H␈↓B4:     ␈↓↓∀p.(istv p ≡ p = T ∨ p = F)␈↓

␈↓ ↓H␈↓B5:     ␈↓↓∀p. isetv not p␈↓

␈↓ ↓H␈↓B6:     ␈↓↓∀p q. isetv(p and q)␈↓

␈↓ ↓H␈↓B7:     ␈↓↓∀p q. isetv(p or q)␈↓

␈↓ ↓H␈↓B8:     ␈↓↓∀p.(not p = ␈↓αif␈↓↓ (p = ␈↓πT␈↓↓) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ F ␈↓αelse␈↓↓ T)␈↓

␈↓ ↓H␈↓B9:     ␈↓↓∀p q.(p and q = ␈↓αif␈↓↓ (p = ␈↓πT␈↓↓) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ F)␈↓

␈↓ ↓H␈↓B10:    ␈↓↓∀p q.(p or q = (␈↓αif␈↓↓ p = ␈↓πT␈↓↓) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ q)␈↓

␈↓ ↓H␈↓B11:    ␈↓↓∀X Y.(X equal Y = ␈↓αif␈↓↓ ¬issexp X ∨ ¬issexp Y ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ X = Y ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ F)␈↓

␈↓ ↓H␈↓B12:    ␈↓↓∀X.(aatom X = ␈↓αif␈↓↓ ¬issexp X ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat␈↓↓ X ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ F)␈↓,

␈↓ ↓H␈↓and we also need a conditional expression that can take an argument from ␈↓	P␈↓, namely

␈↓ ↓H␈↓B13:    ␈↓↓∀p X Y.(if(p,X,Y) = ␈↓αif␈↓↓ p = ␈↓πT␈↓↓ ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ X ␈↓αelse␈↓↓ Y)␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓occura␈↓␈α
is␈α
proved␈α
total␈α
by␈αapplying␈α
schema␈α
LS1␈α
with␈α
␈↓↓␈↓	F␈↓↓(y)␈α≡␈α
occura(x,y)␈α
≠␈α
␈↓πT␈↓↓␈↓.␈α
 After␈αthis␈α
␈↓↓occur␈↓
␈↓ ↓H␈↓can be shown to satisfy (10).

␈↓ ↓H␈↓␈↓ α_The␈α∂axioms␈α∂L1-L16␈α∂and␈α∂B1-B12␈α∂together␈α∂with␈α∂the␈α∂sentences␈α∂arising␈α∂from␈α∂the␈α∂schemata
␈↓ ↓H␈↓LS1␈αand␈αLS2␈αwill␈αbe␈αcalled␈αthe␈αaxiom␈αsystem␈αLisp0.␈α We␈αwill␈αadjoin␈αone␈αmore␈αaxiom␈αlater␈αto␈αget
␈↓ ↓H␈↓the system Lisp1.

␈↓ ↓H␈↓␈↓ α_The␈αabove␈α
method␈αof␈α
replacing␈αa␈α
recursion␈αby␈αa␈α
first␈αorder␈α
sentence␈αwas␈α
first␈α(I␈αthink)␈α
used
␈↓ ↓H␈↓in (Cartwright 1977).  I'm surprised that it wasn't invented sooner.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 96


␈↓ ↓H␈↓α5. An Extended Example.

␈↓ ↓H␈↓␈↓ α_The␈αSAMEFRINGE␈αproblem␈αis␈αto␈αwrite␈αa␈αprogram␈αthat␈αefficiently␈αdetermines␈αwhether␈αtwo
␈↓ ↓H␈↓S-expressions␈α∞have␈α∞the␈α
same␈α∞fringe,␈α∞i.e.␈α
have␈α∞the␈α∞same␈α
atoms␈α∞in␈α∞the␈α
same␈α∞order.␈α∞ (Some␈α
people
␈↓ ↓H␈↓omit␈αthe␈αNILs␈αat␈αthe␈αends␈αof␈αlists,␈αbut␈α
we␈αwill␈αtake␈αall␈αatoms).␈α Thus␈α((A.B).C)␈αand␈α(A.(B.C))␈α
have
␈↓ ↓H␈↓the␈αsame␈αfringe,␈αnamely␈α(A␈αB␈αC).␈α The␈αobject␈αof␈αthe␈αoriginal␈αproblem␈αwas␈αto␈αprogram␈αit␈αusing␈αa
␈↓ ↓H␈↓minimum␈α
of␈α
storage,␈αand␈α
it␈α
was␈αconjectured␈α
that␈α
co-routines␈αwere␈α
necessary␈α
to␈αdo␈α
it␈α
neatly.␈α We
␈↓ ↓H␈↓shall not discuss that matter here - merely the extensional correctness of one proposed solution.

␈↓ ↓H␈↓␈↓ α_The relevant recursive definitions are

␈↓ ↓H␈↓13)␈↓ α8  ␈↓↓fringe x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓,

␈↓ ↓H␈↓where ␈↓↓u * v␈↓ denotes the result of appending the lists ␈↓↓u␈↓ and ␈↓↓v␈↓ and is defined recursively by

␈↓ ↓H␈↓14)␈↓ α8  ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.

␈↓ ↓H␈↓We are interested in the condition ␈↓↓fringe x = fringe y␈↓.

␈↓ ↓H␈↓␈↓ α_The function to be proved correct is ␈↓↓samefringe[x,y]␈↓ defined by the simultaneous recursion

␈↓ ↓H␈↓15)␈↓ α8  ␈↓↓samefringe[x, y] ← (x = y) ∨ [¬␈↓αat␈↓↓ x ∧ ¬␈↓αat␈↓↓ y ∧ same[gopher x, gopher y]]␈↓,

␈↓ ↓H␈↓16)␈↓ α8  ␈↓↓same[x, y] ← (␈↓αa␈↓↓ x = ␈↓αa␈↓↓ y) ∧ samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ ↓H␈↓where

␈↓ ↓H␈↓17)␈↓ α8  ␈↓↓gopher x ←  ␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x]␈↓.

␈↓ ↓H␈↓␈↓ α_We need to prove that ␈↓↓samefringe␈↓ is total and

␈↓ ↓H␈↓18)␈↓ α8  ␈↓↓∀xy.(samefringe[x,y] ≡ fringe x = fringe y)␈↓.

␈↓ ↓H␈↓␈↓ α_The␈αminimization␈α
schemata␈αof␈α
these␈αfunctions␈α
are␈αirrelevant,␈α
because␈αwe␈α
will␈αprove␈αthat␈α
the
␈↓ ↓H␈↓functions␈αare␈αall␈αtotal␈αexcept␈αthat␈αwe␈αwon't␈αprove␈αanything␈αabout␈αthe␈αresult␈αof␈αapplying␈α␈↓↓gopher␈↓␈αto
␈↓ ↓H␈↓an atom.  The functional equations are

␈↓ ↓H␈↓19)␈↓ α8  ␈↓↓∀x.(fringe x = ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓),

␈↓ ↓H␈↓20)␈↓ α8  ␈↓↓∀u v.(u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v])␈↓.

␈↓ ↓H␈↓21)␈↓ α8␈α∂ ␈↓↓∀x␈α∂y.(samefringe[x,␈α∂y]␈α∂=␈α⊂x␈α∂equal␈α∂y␈α∂or␈α∂[not␈α∂aat␈α⊂x␈α∂and␈α∂not␈α∂aat␈α∂y␈α∂and␈α⊂same[gopher␈α∂x,
␈↓ ↓H␈↓↓gopher y]])␈↓,

␈↓ ↓H␈↓22)␈↓ α8 ␈↓↓∀x y.(same[x, y] = ␈↓αa␈↓↓ x equal ␈↓αa␈↓↓ y and samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ ↓H␈↓23)␈↓ α8 ␈↓↓∀x.(gopher x =  ␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x])␈↓.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 97


␈↓ ↓H␈↓Note␈α∞that␈α
because␈α∞␈↓↓samefringe␈↓␈α
and␈α∞␈↓↓same␈↓␈α
are␈α∞recursively␈α
defined␈α∞predicates␈α
which␈α∞have␈α∞not␈α
been
␈↓ ↓H␈↓proved␈α
total,␈α
their␈α
functional␈α
equations␈α
must␈α
use␈α
the␈α
imitation␈α
propositional␈α∞functions␈α
involving
␈↓ ↓H␈↓the extended truth values.

␈↓ ↓H␈↓␈↓ α_We␈αshall␈αnot␈α
give␈αfull␈αproofs␈αbut␈α
merely␈αthe␈αinduction␈αpredicates␈α
and␈αa␈αfew␈α
indications␈αof
␈↓ ↓H␈↓the algebraic transformations.  We begin with a lemma about ␈↓↓gopher␈↓.

␈↓ ↓H␈↓24)␈↓ α8 ␈↓↓∀x y.(issexp gopher[x.y] ∧ ␈↓αat␈↓↓ ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.

␈↓ ↓H␈↓␈↓ α_This lemma can be proved by S-expression structural induction using the predicate

␈↓ ↓H␈↓25)␈↓ α8 ␈↓↓P(x) ≡ ∀y.ok(x,y)␈↓,

␈↓ ↓H␈↓where ␈↓↓ok(x,y)␈↓ is defined by

␈↓ ↓H␈↓26)␈↓ α8␈↓↓∀x y.(ok(x,y) ≡ issexp gopher[x.y] ∧ ␈↓αat␈↓↓ ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.

␈↓ ↓H␈↓In␈α#the␈α#course␈α"of␈α#the␈α#proof,␈α#we␈α"use␈α#the␈α#associativity␈α"of␈α#*␈α#and␈α#the␈α"formula
␈↓ ↓H␈↓␈↓↓fringe[x.y] = fringe x * fringe y␈↓.␈α
 The␈α
lemma␈α
was␈α
expressed␈α
using␈α
␈↓↓gopher[x.y]␈↓␈α
in␈α
order␈α∞to␈α
avoid
␈↓ ↓H␈↓considering␈α
atomic␈αarguments␈α
for␈α␈↓↓gopher␈↓,␈α
but␈αit␈α
could␈α
have␈αequally␈α
well␈αbe␈α
proved␈αabout␈α
␈↓↓gopher x␈↓
␈↓ ↓H␈↓with the condition ␈↓↓¬␈↓αat␈↓↓ x␈↓.

␈↓ ↓H␈↓␈↓ α_Another␈αproof␈αcan␈αbe␈αgiven␈αusing␈αthe␈αcourse-of-values␈αinduction␈αschema␈αfor␈αintegers.␈α We
␈↓ ↓H␈↓write this schema

␈↓ ↓H␈↓ICV:    ␈↓↓∀n.(∀m.(m < n ⊃ P(m)) ⊃ P(n)) ⊃ ∀n.P(n)␈↓,

␈↓ ↓H␈↓where␈α␈↓↓m␈↓␈αand␈α␈↓↓n␈↓␈α
range␈αover␈αnon-negative␈αintegers.␈α
 Exactly␈αthe␈αsame␈αschema␈α
expresses␈αtransfinite
␈↓ ↓H␈↓induction;␈αwe␈α
need␈αonly␈α
imagine␈αthe␈αvariables␈α
ranging␈αover␈α
all␈αordinals␈αless␈α
than␈αa␈α
given␈αone␈α-␈α
in
␈↓ ↓H␈↓this case ␈↓	w␈↓, but equally well ␈↓	w␈↓#
w␈↓#␈↓ or ε␈↓β0␈↓.  We also use the function ␈↓↓size x␈↓ defined by

␈↓ ↓H␈↓27)␈↓ α8 ␈↓↓size x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ size ␈↓αa␈↓↓ x + size ␈↓αd␈↓↓ x␈↓

␈↓ ↓H␈↓satisfying the obvious functional equation.  Our induction predicate is then

␈↓ ↓H␈↓28)␈↓ α8 ␈↓↓P(n) ≡ ∀x y.(size x = n ⊃ ok(x,y))␈↓.

␈↓ ↓H␈↓␈↓ α_For our proof about ␈↓↓samefringe␈↓ we need one more lemma about ␈↓↓gopher␈↓, namely

␈↓ ↓H␈↓29)␈↓ α8 ␈↓↓∀x y.(size gopher[x.y] = size[x.y]␈↓.

␈↓ ↓H␈↓␈↓ α_This␈α→can␈α_be␈α→proved␈α→by␈α_either␈α→of␈α_the␈α→above␈α→inductive␈α_methods␈α→or␈α→by␈α_including
␈↓ ↓H␈↓␈↓↓size gopher[x.y] = size[x.y]␈↓ in the induction hypothesis ␈↓↓ok[x,y]␈↓.

␈↓ ↓H␈↓␈↓ α_The statement about samefringe is

␈↓ ↓H␈↓30)␈↓ α8 ␈↓↓∀x y.(issexp samefringe[x,y] ∧ samefringe[x,y] = T ≡ fringe x = fringe y)␈↓,

␈↓ ↓H␈↓and it is most easily proved by induction on ␈↓↓size x + size y␈↓ using the predicate
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 98


␈↓ ↓H␈↓31)␈↓ α8␈α␈↓↓P(n)␈α≡␈α
∀x␈αy.(n␈α=␈α
size␈αx␈α+␈α
size␈αy␈α⊃␈α
issexp␈αsamefringe[x,y]␈α∧␈α
(samefringe[x,y]␈α=␈αT␈α≡␈α
fringe
␈↓ ↓H␈↓↓x = fringe y))␈↓.

␈↓ ↓H␈↓It␈α
can␈αalso␈α
be␈αproved␈α
using␈α
the␈αwell-foundedness␈α
of␈αlexicographic␈α
ordering␈α
of␈αthe␈α
list␈α␈↓↓<x␈α
␈↓αa␈↓↓␈αx>␈↓,␈α
but
␈↓ ↓H␈↓then we must decide what lexicographic orderings to include in our axiom system.

␈↓ ↓H␈↓␈↓ α_Transfinite␈α
induction␈α
is␈α∞also␈α
useful,␈α
and␈α∞can␈α
be␈α
illustrated␈α∞with␈α
a␈α
variant␈α∞␈↓↓samefringe␈↓␈α
that
␈↓ ↓H␈↓does everything in one complicated recursive definition, namely

␈↓ ↓H␈↓32)␈↓ α8␈α␈↓↓samefringe[x,y]␈α=␈α(x␈αequal␈α
y)␈αor␈αnot␈αaat␈αx␈αand␈α
not␈αaat␈αy␈αand␈α[␈↓αif␈↓↓␈α␈↓αat␈↓↓␈α
␈↓αa␈↓↓␈αx␈α␈↓αthen␈↓↓␈α[␈↓αif␈↓↓␈α␈↓αat␈↓↓␈αy␈α
␈↓αthen␈↓↓
␈↓ ↓H␈↓↓␈↓αa␈↓↓␈α
x␈α
equal␈α
␈↓αa␈↓↓␈α
y␈α
and␈α
samefringe[␈↓αd␈↓↓␈α
x,␈α
␈↓αd␈↓↓␈α
y]␈α
␈↓αelse␈↓↓␈α
samefringe[x,␈α
␈↓αaa␈↓↓␈α
y␈α
.␈α
[␈↓αda␈↓↓␈α
y␈α
.␈α
␈↓αd␈↓↓␈α
y]]]␈α
␈↓αelse␈↓↓␈αsamefringe[␈↓αaa␈↓↓␈α
x
␈↓ ↓H␈↓↓. [␈↓αda␈↓↓ x .␈↓αd␈↓↓ x], y]␈↓.

␈↓ ↓H␈↓The transfinite induction predicate then has the form

␈↓ ↓H␈↓33)␈↓ α8␈α∂␈↓↓P(n)␈α∞≡␈α∂∀x␈α∞y.[n␈α∂=␈α∂␈↓	w␈↓↓(size␈α∞x␈α∂+␈α∞size␈α∂y)␈α∂+␈α∞size␈α∂␈↓αa␈↓↓␈α∞x␈α∂+␈α∂size␈α∞␈↓αa␈↓↓␈α∂y␈α∞⊃␈α∂issexp␈α∂samefringe[x,y]␈α∞∧
␈↓ ↓H␈↓↓(samefringe[x,y] = T ≡ fringe x = fringe y)]␈↓.

␈↓ ↓H␈↓␈↓ α_An␈αeasier␈αexample␈αrequiring␈α
induction␈αup␈αto␈α␈↓	w␈↓∧2␈↓␈α
is␈αproving␈αthe␈αtermination␈αof␈α
Ackermann's
␈↓ ↓H␈↓function which has the functional equation

␈↓ ↓H␈↓2034)␈↓ α8 ␈↓↓∀m n.(A(m,n) = ␈↓αif␈↓↓ m = 0 ␈↓αthen␈↓↓ n+1 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ A(m-1,0) ␈↓αelse␈↓↓ A(m-1,A(m,n-1)))␈↓.

␈↓ ↓H␈↓The statement to be proved is

␈↓ ↓H␈↓2035)␈↓ α8 ␈↓↓∀.( < ␈↓	w␈↓∧2␈↓↓ ∧  = ␈↓	w␈↓↓m + n ⊃ isint A(m,n))␈↓.

␈↓ ↓H␈↓The␈αproof␈αis␈αstraightforward,␈αbecause␈α␈↓	w␈↓↓(m-1) < ␈↓	w␈↓↓m+n␈↓␈αand␈α␈↓	w␈↓↓m+(n-1) < ␈↓	w␈↓↓m+n␈↓,␈αso␈αwe␈α
can␈αassume
␈↓ ↓H␈↓␈↓↓isint A(m-1,0)␈↓␈α∂and␈α⊂␈↓↓isint A(m,n-1)␈↓.␈α∂ From␈α⊂the␈α∂latter,␈α⊂it␈α∂follows␈α⊂that␈α∂␈↓	w␈↓↓(m-1)+A(m,n-1) < ␈↓	w␈↓↓m+n␈↓
␈↓ ↓H␈↓which completes the induction step.

␈↓ ↓H␈↓␈↓ α_We␈α↔would␈α↔like␈α↔to␈α↔prove␈α↔that␈α↔the␈α↔amount␈α↔of␈α↔storage␈α↔used␈α↔in␈α↔the␈α↔computation␈α⊗of
␈↓ ↓H␈↓␈↓↓samefringe[x,y]␈↓␈αaside␈α
from␈αthat␈αoccupied␈α
by␈α␈↓↓x␈↓␈α
and␈α␈↓↓y,␈↓␈αnever␈α
exceeds␈αthe␈αsum␈α
of␈αthe␈α
numbers␈αof
␈↓ ↓H␈↓␈↓↓car␈↓s␈αrequired␈αto␈α
reach␈αcorresponding␈αatoms␈α
in␈α␈↓↓x␈↓␈αand␈α
␈↓↓y.␈↓␈α Unfortunately,␈αwe␈α
can't␈αeven␈αexpress␈α
that
␈↓ ↓H␈↓fact,␈αbecause␈αwe␈α
are␈αaxiomatizing␈αthe␈αprograms␈α
as␈αfunctions,␈αand␈αthe␈α
amount␈αof␈αstorage␈αused␈α
does
␈↓ ↓H␈↓not␈α∞depend␈α∞merely␈α∞on␈α∂the␈α∞function␈α∞being␈α∞computed;␈α∞it␈α∂depends␈α∞on␈α∞the␈α∞method␈α∂of␈α∞computation.
␈↓ ↓H␈↓We␈αmay␈α
regard␈αsuch␈αthings␈α
as␈α␈↓↓intensional␈↓␈αproperties,␈α
but␈αany␈αcorrespondence␈α
with␈αthe␈α
notion␈αof
␈↓ ↓H␈↓intensional properties in intensional logic remains to be established.


␈↓ ↓H␈↓α6. The Minimization Schema.

␈↓ ↓H␈↓␈↓ α_The␈αfunctional␈αequation␈α
of␈αa␈αprogram␈αdoesn't␈α
completely␈αcharacterize␈αit.␈α For␈α
example,␈αthe
␈↓ ↓H␈↓program

␈↓ ↓H␈↓36)␈↓ α8 ␈↓↓f1 x ← f1 x␈↓

␈↓ ↓H␈↓leads to the sentence
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 99


␈↓ ↓H␈↓37)␈↓ α8 ␈↓↓∀x.(f1 x = f1 x)␈↓

␈↓ ↓H␈↓which␈αprovides␈α
no␈αinformation␈α
although␈αthe␈α
function␈α␈↓↓f␈↓␈α
is␈αundefined␈α
for␈αall␈α
␈↓↓x.␈↓␈α This␈α
is␈αnot␈α
always
␈↓ ↓H␈↓the case, since the program

␈↓ ↓H␈↓38)␈↓ α8 ␈↓↓f2 x ← (f2 x).␈↓NIL␈↓↓␈↓

␈↓ ↓H␈↓has the functional equation

␈↓ ↓H␈↓39)␈↓ α8 ␈↓↓∀x.(f2 x = (f2 x).␈↓NIL␈↓↓)␈↓.

␈↓ ↓H␈↓from which ␈↓↓∀x.¬issexp f2(x)␈↓ can be proved by induction.

␈↓ ↓H␈↓␈↓ α_In␈α⊃order␈α⊂to␈α⊃characterize␈α⊃recursive␈α⊂programs,␈α⊃we␈α⊃need␈α⊂some␈α⊃way␈α⊃of␈α⊂asking␈α⊃for␈α⊃the␈α⊂least
␈↓ ↓H␈↓defined solution of the functional equation.

␈↓ ↓H␈↓␈↓ α_Suppose the program is

␈↓ ↓H␈↓40)␈↓ α8 ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓

␈↓ ↓H␈↓yielding the functional equation

␈↓ ↓H␈↓41)␈↓ α8 ␈↓↓∀x.(f x = ␈↓	t␈↓↓[f](x)␈↓.

␈↓ ↓H␈↓The ␈↓↓minimization schema␈↓ is then

␈↓ ↓H␈↓42)␈↓ α8 ␈↓↓∀x.(isD ␈↓	t␈↓↓[␈↓	f␈↓↓](x) ⊃ ␈↓	f␈↓↓ x = ␈↓	t␈↓↓[␈↓	f␈↓↓](x)) ⊃ ∀x.(isD f x ⊃ ␈↓	f␈↓↓ x = f x)␈↓,

␈↓ ↓H␈↓where the predicate ␈↓↓isD␈↓ asserts that its argument is in the domain ␈↓↓D␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α∞␈↓↓minimization␈α
schema␈↓␈α∞can␈α
be␈α∞abbreviated␈α
by␈α∞introducing␈α
Scott's␈α∞partial␈α
ordering␈α∞␈↓πb␈↓␈α
on
␈↓ ↓H␈↓D␈↓∧+␈↓.  We define

␈↓ ↓H␈↓43)␈↓ α8␈↓↓∀X Y.(X ␈↓πb␈↓↓ Y ≡ X = ␈↓πT␈↓↓ ∨ X = Y)␈↓,

␈↓ ↓H␈↓so␈αthat␈αthe␈αonly␈αproper␈αordering␈αis␈αthat␈α␈↓πT␈↓␈αis␈αless␈αthan␈αeverything␈αelse.␈α We␈αalso␈αuse␈αthe␈αsymbol␈α␈↓πd␈↓.
␈↓ ↓H␈↓The minimization schema then becomes

␈↓ ↓H␈↓44)␈↓ α8 ␈↓↓∀x.(␈↓	t␈↓↓[␈↓	f␈↓↓](x) ␈↓πb␈↓↓ ␈↓	f␈↓↓(x)) ⊃ ∀x.(f(x) ␈↓πb␈↓↓ ␈↓	f␈↓↓(x))␈↓,

␈↓ ↓H␈↓which makes it more apparent that the minimization schema asserts that ␈↓↓f␈↓ is minimal.

␈↓ ↓H␈↓␈↓ α_In the ␈↓↓subst␈↓ example, the schema is

␈↓ ↓H␈↓45)␈↓ α8␈↓↓∀x␈α
y␈αz.(␈↓	f␈↓↓(x,y,z)␈α
␈↓πd␈↓↓␈α
␈↓αif␈↓↓␈α␈↓αat␈↓↓␈α
z␈α
␈↓αthen␈↓↓␈α(␈↓αif␈↓↓␈α
z␈α=␈α
y␈α
␈↓αthen␈↓↓␈αx␈α
␈↓αelse␈↓↓␈α
z)␈α␈↓αelse␈↓↓␈α
␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α
z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈αz))␈α
⊃␈α∀x␈α
y
␈↓ ↓H␈↓↓z.(␈↓	f␈↓↓(x,y,z) ␈↓πd␈↓↓ subst(x,y,z))␈↓,

␈↓ ↓H␈↓which has also the longer form
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *10


␈↓ ↓H␈↓46)␈↓ α8␈α⊂␈↓↓∀x␈α⊂y␈α⊂z.(issexp␈α⊂(␈↓αif␈↓↓␈α⊂␈↓αat␈↓↓␈α∂z␈α⊂␈↓αthen␈↓↓␈α⊂(␈↓αif␈↓↓␈α⊂z␈α⊂=␈α⊂y␈α⊂␈↓αthen␈↓↓␈α∂x␈α⊂␈↓αelse␈↓↓␈α⊂z)␈α⊂␈↓αelse␈↓↓␈α⊂␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α⊂z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α⊂z))␈α∂⊃
␈↓ ↓H␈↓↓(␈↓	f␈↓↓(x,y,z)␈α∞=␈α∞␈↓αif␈↓↓␈α∞␈↓αat␈↓↓␈α∞z␈α
␈↓αthen␈↓↓␈α∞(␈↓αif␈↓↓␈α∞z␈α∞=␈α∞y␈α
␈↓αthen␈↓↓␈α∞x␈α∞␈↓αelse␈↓↓␈α∞z)␈α∞␈↓αelse␈↓↓␈α
␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α∞z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α∞z)))␈α∞⊃␈α∞∀x␈α∞y␈α
z.(issexp
␈↓ ↓H␈↓↓subst(x,y,z) ⊃ ␈↓	f␈↓↓(x,y,z) = subst(x,y,z))␈↓.

␈↓ ↓H␈↓␈↓ α_In␈αthe␈αschema␈α␈↓	f␈↓␈αis␈αa␈αfree␈αfunction␈αvariable␈αof␈αthe␈αappropriate␈αnumber␈αof␈αarguments.␈α The
␈↓ ↓H␈↓schema is just a translation into first order logic of Park's (1970) theorem

␈↓ ↓H␈↓47)␈↓ α8 ␈↓↓␈↓	f␈↓↓ ␈↓πd␈↓↓ ␈↓	t␈↓↓[␈↓	f␈↓↓] ⊃ ␈↓	f␈↓↓ ␈↓πd␈↓↓ Y[␈↓	t␈↓↓]␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α
simplest␈α
application␈α
of␈αthe␈α
schema␈α
is␈α
to␈αshow␈α
that␈α
the␈α
␈↓↓f1␈↓␈α
defined␈αby␈α
(36)␈α
is␈α
never␈αan␈α
S-
␈↓ ↓H␈↓expression.  The schema becomes

␈↓ ↓H␈↓48)␈↓ α8 ␈↓↓∀x.(␈↓	f␈↓↓ x ␈↓πd␈↓↓ ␈↓	f␈↓↓ x) ⊃ ∀x.(␈↓	f␈↓↓ x ␈↓πd␈↓↓ f1 x)␈↓,

␈↓ ↓H␈↓and we take

␈↓ ↓H␈↓49)␈↓ α8 ␈↓↓␈↓	f␈↓↓ x = ␈↓πT␈↓↓␈↓.

␈↓ ↓H␈↓The␈αleft␈αside␈αof␈α(48)␈αis␈αidentically␈αtrue,␈αand,␈αremembering␈αthat␈α␈↓πT␈↓␈αis␈αnot␈αan␈αS-expression,␈αthe␈αright
␈↓ ↓H␈↓side tells us that ␈↓↓f1 x␈↓ is never an S-expression.

␈↓ ↓H␈↓␈↓ α_The␈αminimization␈αschema␈αcan␈αsometimes␈αbe␈αused␈αto␈αshow␈αpartial␈αcorrectness.␈α For␈αexample,
␈↓ ↓H␈↓the well known 91-function is defined by the recursive program over the integers

␈↓ ↓H␈↓50)␈↓ α8 ␈↓↓f91 x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ f91 f91(x + 11)␈↓.

␈↓ ↓H␈↓The goal is to show that

␈↓ ↓H␈↓51)␈↓ α8 ␈↓↓∀x.(f91 x = ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91)␈↓.

␈↓ ↓H␈↓We apply the minimization schema with

␈↓ ↓H␈↓52)␈↓ α8 ␈↓↓␈↓	f␈↓↓ x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91␈↓,

␈↓ ↓H␈↓and␈α
it␈αcan␈α
be␈α
shown␈αby␈α
an␈α
explicit␈αcalculation␈α
without␈α
induction␈αthat␈α
the␈α
premiss␈αof␈α
the␈αschema␈α
is
␈↓ ↓H␈↓satisfied, and this shows that ␈↓↓f91,␈↓ whenever defined has the desired value.

␈↓ ↓H␈↓␈↓ α_The␈α
method␈α
of␈α
recursion␈α
induction␈α
(∪cCarthy␈α1963)␈α
is␈α
also␈α
an␈α
immediate␈α
application␈αof␈α
the
␈↓ ↓H␈↓minimization␈α
schema.␈α
 If␈α
we␈α
show␈α
that␈α
two␈αfunctions␈α
satisfy␈α
the␈α
schema␈α
of␈α
a␈α
recursive␈αprogram,
␈↓ ↓H␈↓we␈α
show␈α
that␈αthey␈α
both␈α
equal␈α
the␈αfunction␈α
computed␈α
by␈α
the␈αprogram␈α
on␈α
whereever␈α
the␈αfunction␈α
is
␈↓ ↓H␈↓defined.

␈↓ ↓H␈↓␈↓ α_The␈α
utility␈α
of␈α
the␈α
minimization␈αschema␈α
for␈α
proving␈α
partial␈α
correctness␈α
or␈αnon-termination
␈↓ ↓H␈↓depends␈α∂on␈α∂our␈α∞ability␈α∂to␈α∂name␈α∂suitable␈α∞comparison␈α∂functions.␈α∂ f1␈α∞and␈α∂f91␈α∂were␈α∂easily␈α∞treated,
␈↓ ↓H␈↓because␈α⊃the␈α⊃necessary␈α⊃comparison␈α⊃functions␈α⊃could␈α⊃be␈α⊃given␈α⊃explicitly␈α⊃without␈α⊃recursion.␈α⊂ Any
␈↓ ↓H␈↓extension␈αof␈αthe␈αlanguage␈αthat␈αprovides␈αnew␈αtools␈αfor␈αnaming␈αcomparison␈αfunctions,␈αe.g.␈αgoing␈αto
␈↓ ↓H␈↓higher order logic, will improve our ability to use the schema in proofs.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *11


␈↓ ↓H␈↓␈↓ α_(42)␈α∂can␈α∞be␈α∂regarded␈α∞as␈α∂an␈α∞axiom␈α∂schema␈α∞involving␈α∂a␈α∞second␈α∂order␈α∞function␈α∂variable␈α∞␈↓	t␈↓.
␈↓ ↓H␈↓What␈αcan␈α
be␈αsubstituted␈α
for␈α␈↓	t␈↓␈α
is␈αa␈α quantifier␈α
free␈αλ-expression␈α
in␈αa␈α
first␈αorder␈αfunction␈α
variable.
␈↓ ↓H␈↓It␈α
may␈α
be␈α
interesting␈α
to␈α
study␈α
the␈α
sets␈α
of␈α
first␈α
order␈α
sentences␈α
that␈α
can␈α
be␈α
generated␈α
by␈αsuch␈α
second
␈↓ ↓H␈↓order␈αsentence␈αschemata.␈α Presumably,␈αsets␈αof␈αsentences␈αcan␈αbe␈αgenerated␈αin␈αthis␈αway␈αthat␈αcannnot
␈↓ ↓H␈↓be generated by schemata with only first order function variables.



␈↓ ↓H␈↓α7. Proof Methods as Axiom Schemata

␈↓ ↓H␈↓␈↓ α_Representing␈α
recursive␈α
definitions␈α
in␈αfirst␈α
order␈α
logic␈α
permits␈αus␈α
to␈α
express␈α
some␈αwell␈α
known
␈↓ ↓H␈↓methods for proving partial correctness as axiom schemata of first order logic.

␈↓ ↓H␈↓␈↓ α_For example, suppose we want to prove that if the input ␈↓↓x␈↓ of a function ␈↓↓f␈↓ defined by

␈↓ ↓H␈↓53)␈↓ α8  ␈↓↓f x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ f h x␈↓

␈↓ ↓H␈↓satisfies␈α␈↓↓␈↓	F␈↓↓(x)␈↓,␈αthen␈αif␈αthe␈αfunction␈αterminates,␈αthe␈αoutput␈α␈↓↓f(x)␈↓␈αwill␈αsatisfy␈α␈↓	Y␈↓↓(x,f(x))␈↓.␈α We␈αappeal␈αto
␈↓ ↓H␈↓the following ␈↓↓axiom schema of inductive assertions␈↓:

␈↓ ↓H␈↓54)␈↓ α8  ␈↓↓∀x.(␈↓	F␈↓↓(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ ␈↓	Y␈↓↓(x,y) ␈↓αelse␈↓↓ q(x,␈↓π ␈↓↓h y))
␈↓ ↓H␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ isD f x ⊃ ␈↓	Y␈↓↓(x,f x))␈↓


␈↓ ↓H␈↓where␈α␈↓↓isD␈α
f␈αx␈↓␈α
is␈αthe␈α
assertion␈αthat␈α
␈↓↓f(x)␈↓␈αis␈α
in␈αthe␈α
nominal␈αrange␈α
of␈αthe␈α
function␈αdefinition,␈α
i.e.␈αis␈α
an
␈↓ ↓H␈↓integer␈α∞or␈α
an␈α∞S-expression␈α∞as␈α
the␈α∞case␈α
may␈α∞be,␈α∞and␈α
asserts␈α∞that␈α
the␈α∞computation␈α∞terminates.␈α
 In
␈↓ ↓H␈↓order␈α⊂to␈α⊂use␈α⊂the␈α∂schema,␈α⊂we␈α⊂must␈α⊂invent␈α∂a␈α⊂suitable␈α⊂predicate␈α⊂␈↓↓q(x,y)␈↓,␈α∂and␈α⊂this␈α⊂is␈α⊂precisely␈α∂the
␈↓ ↓H␈↓method␈αof␈αinductive␈αassertions.␈α The␈αschema␈αis␈αvalid␈αfor␈αall␈αpredicates␈α␈↓	F␈↓,␈α␈↓	Y␈↓,␈αand␈α␈↓↓q␈↓,␈αand␈αa␈αsimilar
␈↓ ↓H␈↓schema can be written for any collection of mutually recursive definitions that is iterative.

␈↓ ↓H␈↓␈↓ α_The␈α∂method␈α∂of␈α∞␈↓↓subgoal␈α∂induction␈↓␈α∂for␈α∞recursive␈α∂programs␈α∂was␈α∞introduced␈α∂in␈α∂(Manna␈α∞and
␈↓ ↓H␈↓Pnueli␈α∂1970),␈α⊂but␈α∂they␈α∂didn't␈α⊂give␈α∂it␈α⊂a␈α∂name.␈α∂ Morris␈α⊂and␈α∂Wegbreit␈α∂(1977)␈α⊂name␈α∂it,␈α⊂extend␈α∂it
␈↓ ↓H␈↓somewhat,␈α⊂and␈α⊂apply␈α⊂it␈α∂to␈α⊂Algol-like␈α⊂programs.␈α⊂ Unlike␈α∂␈↓↓inductive␈α⊂assertions␈↓,␈α⊂it␈α⊂isn't␈α⊂limited␈α∂to
␈↓ ↓H␈↓iterative definitions.  Thus, for the recursive program

␈↓ ↓H␈↓55)␈↓ α8  ␈↓↓f␈↓β5␈↓↓ x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f␈↓β5␈↓↓ g2 x␈↓,

␈↓ ↓H␈↓where ␈↓↓p␈↓ is assumed total, we have

␈↓ ↓H␈↓56)␈↓ α8  ␈↓↓∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧ ∀x.(␈↓	F␈↓↓(x) ∧ q(x,z) ⊃ ␈↓	Y␈↓↓(x,z))
␈↓ ↓H␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ isD(f(x)) ⊃ ␈↓	Y␈↓↓(x,f(x)))␈↓

␈↓ ↓H␈↓␈↓ α_We␈α∞can␈α∞express␈α∞these␈α∞methods␈α∞as␈α∂axiom␈α∞schemata,␈α∞because␈α∞we␈α∞have␈α∞the␈α∞predicate␈α∂␈↓↓isD␈↓␈α∞to
␈↓ ↓H␈↓express␈α∞termination.␈α∞ The␈α∞minimization␈α∞schema␈α∞itself␈α∞can␈α∞be␈α∞proved␈α∞by␈α∞subgoal␈α∞induction.␈α
 We
␈↓ ↓H␈↓need only take ␈↓↓␈↓	F␈↓↓(x) ≡ ␈↓αtrue␈↓ and ␈↓	Y␈↓↓(x,y) ≡ (y = ␈↓	f␈↓↓(x))␈↓ and ␈↓↓q(x,y) ≡ (y = ␈↓	f␈↓↓(x))␈↓.

␈↓ ↓H␈↓␈↓ α_General␈α
rules␈αfor␈α
going␈αfrom␈α
a␈αrecursive␈α
program␈α
to␈αwhat␈α
amounts␈αto␈α
the␈αsubgoal␈α
induction
␈↓ ↓H␈↓schema␈α
are␈α
given␈α
in␈α
(Manna␈α
and␈α
Pnueli␈α
1970)␈α
and␈α
(Morris␈α
and␈α
Wegbreit␈α
1977);␈α
we␈α
need␈α
only␈α
add
␈↓ ↓H␈↓a conclusion involving the ␈↓↓isD␈↓ predicate to the Manna's and Pnueli formula ␈↓↓W␈↓βP␈↓.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *12


␈↓ ↓H␈↓␈↓ α_However,␈α∞we␈α
can␈α∞characterize␈α
subgoal␈α∞induction␈α
as␈α∞an␈α
axiom␈α∞schema.␈α
 Namely,␈α∞we␈α
define
␈↓ ↓H␈↓␈↓	t␈↓↓'[q]␈↓ as an extension of ␈↓	t␈↓ mapping relations into relations.  Thus if

␈↓ ↓H␈↓57)␈↓ α8  ␈↓↓␈↓	t␈↓↓[f](x) = ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f g2 x␈↓,

␈↓ ↓H␈↓we have

␈↓ ↓H␈↓58)␈↓ α8  ␈↓↓␈↓	t␈↓↓'[q](x,y) ≡ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ (y = h x) ␈↓αelse␈↓↓ ∃z.(q(g2 x,z) ∧ y = g1 z)␈↓.

␈↓ ↓H␈↓In general we have

␈↓ ↓H␈↓59)␈↓ α8  ␈↓↓∀xy.(␈↓	t␈↓↓'[q](x,y) ⊃ q(x,y)) ⊃ ∀x.(isD f x ⊃ q(x,f x))␈↓,

␈↓ ↓H␈↓from␈α
which␈α
the␈α
subgoal␈α∞induction␈α
rule␈α
follows␈α
immediately␈α
given␈α∞the␈α
properties␈α
of␈α
␈↓	F␈↓␈α
and␈α∞␈↓	Y␈↓.␈α
 I
␈↓ ↓H␈↓am indebted to Wolfgang Polak (oral communication) for help in elucidating this relationship.

␈↓ ↓H␈↓␈↓αWARNING␈↓:␈αThe␈αrest␈α
of␈αthis␈αsection␈α
is␈αstill␈αsomewhat␈α
conjectural␈αand␈αis␈α
subject␈αto␈αchange.␈α
 There
␈↓ ↓H␈↓may be bugs.

␈↓ ↓H␈↓␈↓ α_The␈αextension␈α
␈↓↓␈↓	t␈↓↓'[q]␈↓␈αcan␈α
be␈αdetermined␈α
as␈αfollows:␈α
Introduce␈αinto␈α
the␈αlogic␈α
the␈αnotion␈α
of␈αa
␈↓ ↓H␈↓␈↓↓multi-term␈↓␈α
which␈αis␈α
formed␈αin␈α
the␈αsame␈α
way␈α
as␈αa␈α
term␈αbut␈α
allows␈αrelations␈α
written␈α
as␈αfunctions.
␈↓ ↓H␈↓For␈α∀the␈α∀present␈α∃we␈α∀won't␈α∀interpret␈α∃them␈α∀but␈α∀merely␈α∀give␈α∃rules␈α∀for␈α∀introducing␈α∃them␈α∀and
␈↓ ↓H␈↓subsequently␈α
eliminating␈αthem␈α
again␈α
to␈αget␈α
an␈α
ordinary␈αformula.␈α
 Thus␈α
we␈αwill␈α
write␈α
␈↓↓q<e>␈↓␈αwhere␈α
␈↓↓e␈↓
␈↓ ↓H␈↓is␈αany␈αterm␈αor␈αmulti-term.␈α We␈αthen␈αform␈α
␈↓↓␈↓	t␈↓↓'[q]␈↓␈αexactly␈αin␈αthe␈αsame␈αway␈α␈↓↓␈↓	t␈↓↓[f]␈↓␈αwas␈α
formed.␈α Thus
␈↓ ↓H␈↓for the 91-function we have

␈↓ ↓H␈↓60)␈↓ α8  ␈↓↓␈↓	t␈↓↓'[q](x) = ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>␈↓.

␈↓ ↓H␈↓The␈α⊃pointy␈α⊃brackets␈α⊃indicate␈α⊃that␈α⊃we␈α⊃are␈α⊃"applying"␈α⊃a␈α⊃relation.␈α⊃ We␈α⊃now␈α⊃evaluate␈α⊂␈↓↓␈↓	t␈↓↓'[q](x,y)␈↓
␈↓ ↓H␈↓formally as follows:

␈↓ ↓H␈↓61)␈↓ α8  ␈↓↓␈↓	t␈↓↓'[q](x,y)   ≡ (␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>)(y)

␈↓ ↓H␈↓↓                        ≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ q(q<x+11>,y)

␈↓ ↓H␈↓↓                        ≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ ∃z.(q(x+11,z) ∧ q(z,y))␈↓.

␈↓ ↓H␈↓This␈α⊂last␈α⊂formula␈α∂has␈α⊂no␈α⊂pointy␈α∂brackets␈α⊂and␈α⊂is␈α∂just␈α⊂the␈α⊂formula␈α∂that␈α⊂would␈α⊂be␈α⊂obtained␈α∂by
␈↓ ↓H␈↓Manna and Pnueli or Morris and Wegbreit.  The rules are as follows:

␈↓ ↓H␈↓␈↓ α_(i)␈α∂␈↓↓␈↓	t␈↓↓'[q](x)␈↓␈α∂is␈α∂just␈α∂like␈α∂␈↓↓␈↓	t␈↓↓[f](x)␈↓␈α∂except␈α∂that␈α∂␈↓↓q␈↓␈α∂replaces␈α∂␈↓↓f␈↓␈α∂and␈α∂takes␈α∂its␈α∂arguments␈α∂in␈α∞pointy
␈↓ ↓H␈↓brackets.

␈↓ ↓H␈↓␈↓ α_(ii) an ordinary term ␈↓↓e␈↓ applied to ␈↓↓y␈↓ becomes ␈↓↓y = e␈↓.

␈↓ ↓H␈↓␈↓ α_(ii) ␈↓↓q<e>(y)␈↓ becomes ␈↓↓q(e,y)␈↓.

␈↓ ↓H␈↓␈↓ α_(ii)␈α∪␈↓↓P(q<e>)␈↓␈α∪becomes␈α∪␈↓↓∃z.q(e,z) ∧ P(z)␈↓␈α∪when␈α∩␈↓↓P(q<e>)␈↓␈α∪occurs␈α∪positively␈α∪in␈α∪␈↓↓␈↓	t␈↓↓'[q](x,y)␈↓␈α∩and
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *13


␈↓ ↓H␈↓becomes␈α⊂␈↓↓∀z.q(e,z) ⊃ P(z)␈↓␈α⊂when␈α⊂the␈α⊂occurrence␈α⊂is␈α⊂negatve.␈α⊂ It␈α⊂is␈α⊂not␈α⊂evident␈α⊃what␈α⊂independent
␈↓ ↓H␈↓semantics should be given to multi-terms.




␈↓ ↓H␈↓α8. Representations Using Finite Approximations.

␈↓ ↓H␈↓␈↓ α_Our␈αsecond␈αapproach␈αto␈αrepresenting␈αrecursive␈αprograms␈αby␈αfirst␈αorder␈αformulas␈αgoes␈αback
␈↓ ↓H␈↓to␈α⊂G␈↓
:␈↓odel␈α⊂(1931,␈α∂1934)␈α⊂who␈α⊂showed␈α∂that␈α⊂primitive␈α⊂recursive␈α∂functions␈α⊂could␈α⊂be␈α⊂so␈α∂represented.
␈↓ ↓H␈↓(Our knowledge of G␈↓
:␈↓odel's work comes from (Kleene 1951)).

␈↓ ↓H␈↓␈↓ α_Kleene␈α(1951)␈α
calls␈αa␈αfunction␈α
␈↓↓f␈↓␈α␈↓↓representable␈↓␈αif␈α
there␈αis␈αan␈α
arithmetic␈αformula␈α␈↓↓A␈↓␈α
with␈αfree
␈↓ ↓H␈↓variables ␈↓↓x␈↓ and ␈↓↓y␈↓ such that

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓∀x y.((y = f(x)) ≡ A)␈↓,

␈↓ ↓H␈↓where␈αan␈αarithmetic␈αformula␈αis␈αbuilt␈αup␈αfrom␈αinteger␈αconstants␈αand␈αvariables␈αusing␈αonly␈αaddition,
␈↓ ↓H␈↓multiplication␈αand␈αbounded␈α
quantification.␈α Kleene␈αshowed␈αthat␈α
all␈αpartial␈αrecursive␈αfunctions␈α
are
␈↓ ↓H␈↓representable.␈α The␈α
proof␈αinvolves␈αG␈↓
:␈↓odel␈α
numbering␈αpossible␈α
computation␈αsequences␈αand␈α
showing
␈↓ ↓H␈↓that␈α
the␈α∞relation␈α
between␈α
sequences␈α∞and␈α
their␈α
elements␈α∞and␈α
the␈α
steps␈α∞of␈α
the␈α
computation␈α∞are␈α
all
␈↓ ↓H␈↓representable.

␈↓ ↓H␈↓␈↓ α_In␈αLisp␈αless␈αmachinery␈α
is␈αneeded,␈αbecause␈αsequences␈αare␈α
Lisp␈αdata,␈αand␈αthe␈αrelation␈α
between
␈↓ ↓H␈↓a␈αsequence␈αand␈αits␈αelements␈αis␈αgiven␈αby␈αbasic␈αLisp␈αfunctions␈αand␈αby␈αthe␈α␈↓↓occurence␈αrelation␈↓␈αdefined
␈↓ ↓H␈↓in section 5 by

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓occur[x,y] ← (x = y) ∨ ¬␈↓αat␈↓↓ y ∧ [occur[x,␈↓αa␈↓↓ y] ∨ occur[x, ␈↓αd␈↓↓ y]]␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓occur␈↓␈α∂is␈α∞the␈α∂only␈α∞recursive␈α∂definition␈α∞we␈α∂shall␈α∂require.␈α∞ Since␈α∂it␈α∞is␈α∂total,␈α∞we␈α∂only␈α∂need␈α∞its
␈↓ ↓H␈↓functional equation to represent it in first order logic.  The functional equation is

␈↓ ↓H␈↓L17:    ␈↓↓∀x y.(occur[x,y] ≡ (x=y) ∨ ¬␈↓αat␈↓↓ y ∧ (occur[x,␈↓αa␈↓↓ y] ∨ occur[x,␈↓αd␈↓↓ y]))␈↓,

␈↓ ↓H␈↓␈↓ α_The␈α⊃axiom␈α⊃system␈α⊃consisting␈α⊂of␈α⊃L1-L17,␈α⊃B1-B12,␈α⊃and␈α⊂the␈α⊃sentences␈α⊃resulting␈α⊃from␈α⊂the
␈↓ ↓H␈↓schemata LS1 and LS2 will be called the axiom system Lisp1.

␈↓ ↓H␈↓␈↓ α_Starting␈α
with␈α
␈↓↓occur␈↓␈α
and␈α
the␈α
basic␈α
Lisp␈αfunctions␈α
and␈α
predicates␈α
we␈α
will␈α
define␈α
three␈αother
␈↓ ↓H␈↓Lisp␈α⊃predicates␈α⊂without␈α⊃recursion.␈α⊂ By␈α⊃␈↓↓u istail v␈↓␈α⊂we␈α⊃mean␈α⊂that␈α⊃␈↓↓u␈↓␈α⊂can␈α⊃be␈α⊂obtained␈α⊃from␈α⊃␈↓↓v␈↓␈α⊂by
␈↓ ↓H␈↓repeated␈α␈↓↓cdr␈↓s.␈α Thus␈αthe␈αtails␈αof␈α(A␈α
B␈αC␈αD)␈αare␈α(A␈αB␈αC␈αD),␈α
(B␈αC␈αD),␈α(C␈αD),␈α(D)␈αand␈α
NIL.␈α The
␈↓ ↓H␈↓natural recursive definition of ␈↓↓istail␈↓ is

␈↓ ↓H␈↓3)␈↓ α8 ␈↓↓u istail v ← (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v)␈↓

␈↓ ↓H␈↓which according to the previous sections would lead to the first order formula

␈↓ ↓H␈↓4)␈↓ α8 ␈↓↓∀u v.(u istail v ≡ (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v))␈↓,
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *14


␈↓ ↓H␈↓but␈α
(4)␈α
is␈α
still␈α
an␈αimplicit␈α
definition␈α
of␈α
␈↓↓istail␈↓,␈α
because␈αthe␈α
function␈α
being␈α
defined␈α
occurs␈α
on␈αboth
␈↓ ↓H␈↓sides of the equivalence sign.  A suitable explicit definition is

␈↓ ↓H␈↓5)␈↓ α8  ␈↓↓∀u v.(u istail v ≡ occur[u,v] ∧ ∀x.(occur[u,x] ∧ occur[x,v] ⊃ x = u ∨ occur[u, ␈↓αd␈↓↓ x]))␈↓.

␈↓ ↓H␈↓Next we shall define membership in a list.  We have

␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓∀x v.(x ε v ≡ ∃u.(u istail v ∧ x = ␈↓αa␈↓↓ u))␈↓.

␈↓ ↓H␈↓Now we define an ␈↓↓a-list␈↓ - a familiar Lisp concept.  We have

␈↓ ↓H␈↓7)␈↓ α8␈α
 ␈↓↓∀w.(isalist␈αw␈α
≡␈α∀x.(x␈α
ε␈αw␈α
⊃␈α¬␈↓αat␈↓↓␈α
x)␈α∧␈α
∀u1␈αu2.(u1␈α
istail␈αw␈α
∧␈αu2␈α
istail␈αw␈α
∧␈α␈↓αaa␈↓↓␈α
u1␈α=␈α
␈↓αaa␈↓↓␈αu2␈α
⊃
␈↓ ↓H␈↓↓u1 = u2))␈↓.

␈↓ ↓H␈↓Thus␈α∞an␈α
␈↓↓a-list␈↓␈α∞is␈α∞a␈α
list␈α∞of␈α
pairs␈α∞such␈α∞that␈α
no␈α∞S-expression␈α
is␈α∞the␈α∞first␈α
element␈α∞of␈α∞two␈α
different
␈↓ ↓H␈↓pairs.␈α⊃ Therefore,␈α⊃a-lists␈α⊃are␈α⊃suitable␈α⊃for␈α⊂representing␈α⊃finite␈α⊃lists␈α⊃of␈α⊃argument-value␈α⊃pairs␈α⊂for
␈↓ ↓H␈↓partial functions.

␈↓ ↓H␈↓␈↓ α_Finally,␈α
we␈α
need␈α
the␈α
familiar␈α
Lisp␈α
function␈α
␈↓↓assoc␈↓␈α
that␈α
is␈α
used␈α
for␈α
looking␈α
up␈α
atoms␈α
on␈α␈↓↓a-
␈↓ ↓H␈↓↓lists␈↓.  Its familiar recursive definition is

␈↓ ↓H␈↓8)␈↓ α8  ␈↓↓assoc(x,w) ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ w ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x = ␈↓αaa␈↓↓ w ␈↓αthen␈↓↓ ␈↓αa␈↓↓ w ␈↓αelse␈↓↓ assoc(x,␈↓αd␈↓↓ w)␈↓,

␈↓ ↓H␈↓but it can be represented by

␈↓ ↓H␈↓9)␈↓ α8  ␈↓↓∀w x y.(x.y = assoc(x,w) ≡ ∃w1.(w1 istail w ∧ x.y = ␈↓αa␈↓↓ w1) ∨ assoc(x,w) = ␈↓NIL␈↓↓)␈↓.

␈↓ ↓H␈↓␈↓ α_Now let ␈↓↓f␈↓ be an arbitrary recursive program defined by

␈↓ ↓H␈↓10)␈↓ α8  ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓

␈↓ ↓H␈↓for␈αsome␈αcontinuous␈αfunctional␈α␈↓	t␈↓.␈α In␈αorder␈αto␈αemphasize␈αthe␈αparallel␈αbetween␈αa␈αpartial␈αfunction␈α
␈↓↓f␈↓
␈↓ ↓H␈↓and an ␈↓↓a-list␈↓ used as a finite approximation, we define

␈↓ ↓H␈↓11)␈↓ α8 ␈↓	t␈↓↓'(w)(x) = ␈↓	t␈↓↓[λz.␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(z,w) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(z,w)](x)␈↓.

␈↓ ↓H␈↓Thus␈α␈↓	t␈↓'␈αis␈αlike␈α␈↓	t␈↓␈αexcept␈αthat␈αwhenever␈α␈↓	t␈↓␈αevaluates␈αits␈αfunctional␈αargument␈α␈↓↓f␈↓␈αat␈αsome␈αvalue␈α␈↓↓z,␈↓␈α␈↓	t␈↓'
␈↓ ↓H␈↓looks up ␈↓↓z␈↓ on the a-list ␈↓↓w.␈↓

␈↓ ↓H␈↓␈↓ α_With this preparation we can write

␈↓ ↓H␈↓12)␈↓ α8␈α ␈↓↓∀x␈α(¬∃y␈αw.(x.y␈α=␈α␈↓αa␈↓↓␈αw␈α∧␈α∀x1␈αy1␈αw1.(w1␈αistail␈αw␈α∧␈αx1.y1␈α=␈α␈↓αa␈↓↓␈αw1␈α⊃␈αy1␈α=␈α␈↓	t␈↓↓'[␈↓αd␈↓↓␈αw1](x1)))␈α⊃
␈↓ ↓H␈↓↓f(x)␈α
=␈α
␈↓πT␈↓↓)␈α
∧␈α
∀y.(∃w.(x.y␈α
=␈α
␈↓αa␈↓↓␈α
w␈α
∧␈α
∀x1␈α
y1␈α
w1.(w1␈α
istail␈α
w␈α
∧␈α
x1.y1␈α
=␈α
␈↓αa␈↓↓␈α
w1␈α
⊃␈α
y1␈α
=␈α
␈↓	t␈↓↓'[␈↓αd␈↓↓␈α
w1](x1))))␈α⊃␈α
f(x)
␈↓ ↓H␈↓↓= y))␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α∞essence␈α
of␈α∞this␈α
formula␈α∞is␈α
simple.␈α∞ ␈↓↓w␈↓␈α
is␈α∞an␈α
a-list␈α∞containing␈α
all␈α∞argument-value␈α
pairs
␈↓ ↓H␈↓that␈α⊂arise␈α⊂in␈α⊂the␈α⊂evaluation␈α∂of␈α⊂␈↓↓f(x).␈↓␈α⊂We␈α⊂require␈α⊂that␈α⊂if␈α∂␈↓↓x␈↓␈α⊂occurs␈α⊂somewhere␈α⊂on␈α⊂␈↓↓w,␈↓␈α⊂the␈α∂pairs
␈↓ ↓H␈↓involved␈α∞in␈α∞the␈α∞evaluation␈α∂of␈α∞␈↓↓f(x)␈↓␈α∞occur␈α∞further␈α∂on␈α∞in␈α∞the␈α∞a-list␈α∂␈↓↓w.␈↓␈α∞ This␈α∞is␈α∞to␈α∂avoid␈α∞allowing
␈↓ ↓H␈↓circular recursions.  If there is no such a-list, then ␈↓↓f(x) = ␈↓πT␈↓↓.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *15


␈↓ ↓H␈↓␈↓ α_If␈α
the␈αlogic␈α
has␈α
a␈αdescription␈α
operator␈α
␈↓	i␈↓,␈αwhere␈α
␈↓	i␈↓↓␈α
x.P(x)␈↓␈αstands␈α
for␈α
the␈α"the␈α
unique␈α
␈↓↓x␈↓␈αsuch
␈↓ ↓H␈↓that ␈↓↓P(x)␈↓ if there is such a unique ␈↓↓x␈↓ and otherwise ␈↓πT␈↓", then (12) can be written

␈↓ ↓H␈↓13)␈↓ α8␈α∂␈↓↓∀x.(f(x)␈α∂=␈α∂␈↓	i␈↓↓␈α∂y.∃w.(x.y␈α∂=␈α∂␈↓αa␈↓↓␈α∂w␈α∂∧␈α∂∀x1␈α∂y1␈α∂w1.(w1␈α∂istail␈α∂w␈α∂∧␈α∂x1.y1␈α∂=␈α∂␈↓αa␈↓↓␈α∂w1␈α∂⊃␈α∂y1␈α∂=␈α∂␈↓	t␈↓↓'[␈↓αd␈↓↓
␈↓ ↓H␈↓↓w1](x1))))␈↓.

␈↓ ↓H␈↓␈↓ α_As an example, consider the Lisp function ␈↓↓ff␈↓ defined recursively by

␈↓ ↓H␈↓14)␈↓ α8 ␈↓↓ff x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ ff ␈↓αa␈↓↓ x␈↓.

␈↓ ↓H␈↓(13) then takes the form

␈↓ ↓H␈↓15)␈↓ α8␈α
∀x.(ff␈αx␈α
=␈α
␈↓	i␈↓↓y.∃w.(x.y␈α=␈α
␈↓αa␈↓↓␈α
w␈α∧␈α
∀x1␈α
y1␈αw1.(w1␈α
istail␈αw␈α
∧␈α
x1.y1␈α=␈α
␈↓αa␈↓↓␈α
w1␈α⊃␈α
y1␈α
=␈α␈↓αif␈↓↓␈α
␈↓αat␈↓↓␈αx1␈α
␈↓αthen␈↓↓
␈↓ ↓H␈↓↓x1 ␈↓αelse␈↓↓ (␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(x1,␈↓αd␈↓↓ w1) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(x1,␈↓αd␈↓↓ w1)))))␈↓.

␈↓ ↓H␈↓␈↓ α_Suppose␈α∞we␈α∞were␈α∞computing␈α∞␈↓↓ff ((A.B).C)␈↓.␈α
 A␈α∞suitable␈α∞␈↓↓w␈↓␈α∞would␈α∞be␈α∞((((A.B).C).A)␈α
((A.B).A)
␈↓ ↓H␈↓(A.A)).

␈↓ ↓H␈↓␈↓ α_It␈α∂might␈α∂be␈α⊂asked␈α∂whether␈α∂␈↓↓occur␈↓␈α∂is␈α⊂necessary.␈α∂ Couldn't␈α∂we␈α∂represent␈α⊂recursive␈α∂programs
␈↓ ↓H␈↓using␈αjust␈α␈↓↓car,␈αcdr,␈αcons␈↓␈αand␈α␈↓↓atom␈↓?␈α No,␈αfor␈αthe␈αfollowing␈αreason.␈α Suppose␈αthat␈αthe␈αfunction␈α␈↓↓f␈↓␈αis
␈↓ ↓H␈↓representable using only the basic Lisp functions without ␈↓↓subexp␈↓, and consider the sentence

␈↓ ↓H␈↓16)␈↓ α8 ␈↓↓∀x.issexp f(x)␈↓,

␈↓ ↓H␈↓asserting␈αthe␈αtotality␈α
of␈α␈↓↓f.␈↓␈αUsing␈α
the␈αrepresentation,␈αwe␈α
can␈αwrite␈α(16)␈α
as␈αa␈αsentence␈αinvolving␈α
only
␈↓ ↓H␈↓the␈α⊂basic␈α⊃Lisp␈α⊂functions␈α⊃and␈α⊂the␈α⊂constant␈α⊃␈↓πT␈↓.␈α⊂ However,␈α⊃may␈α⊂be␈α⊂shown␈α⊃in␈α⊂Appendix␈α⊃I,␈α⊂these
␈↓ ↓H␈↓sentences␈αare␈αdecidable,␈αand␈αtotality␈αisn't.␈α (I'll␈αput␈αthe␈αproof␈αin␈αAppendix␈αI␈αif␈αI␈αcan␈αprove␈αit.␈α At
␈↓ ↓H␈↓this time, I think I've almost got it).

␈↓ ↓H␈↓␈↓ α_In␈α∞case␈α∞of␈α∞functions␈α∞of␈α∞several␈α∞variables,␈α∞(12)␈α∞corresponds␈α∞to␈α∞a␈α∂call-by-value␈α∞computation
␈↓ ↓H␈↓rule␈αwhile␈αthe␈αrepresentations␈αof␈αthe␈αprevious␈αsections␈αcorrespond␈αto␈αcall-by-name␈αor␈αother␈α"safe"
␈↓ ↓H␈↓rules.␈α∞ The␈α∞difference␈α∂is␈α∞not␈α∞important,␈α∂because␈α∞of␈α∞Vuillemin's␈α∂theorem␈α∞that␈α∞any␈α∂strict␈α∞function
␈↓ ↓H␈↓may be computed either according to call-by-name or call-by-value.


␈↓ ↓H␈↓α9. Questions of Incompleteness.

␈↓ ↓H␈↓␈↓ α_Luckham,␈αPark␈αand␈αPaterson␈α(1970)␈αhave␈αshown␈αthat␈αwhether␈αa␈αprogram␈α
schema␈αdiverges
␈↓ ↓H␈↓for␈α∞every␈α∞interpretation,␈α∂whether␈α∞it␈α∞diverges␈α∞for␈α∂some␈α∞interpretation,␈α∞and␈α∞whether␈α∂two␈α∞program
␈↓ ↓H␈↓schemas␈α∀are␈α∪equivalent␈α∀are␈α∀all␈α∪not␈α∀even␈α∪partially␈α∀solvable␈α∀problems.␈α∪ Manna␈α∀(1974)␈α∀has␈α∪a
␈↓ ↓H␈↓thorough␈αdiscussion␈αof␈αthese␈αpoints.␈α In␈αview␈αof␈αthese␈αresults,␈αwhat␈αcan␈αbe␈αexpected␈αfrom␈αour␈αfirst
␈↓ ↓H␈↓order representations?

␈↓ ↓H␈↓␈↓ α_First␈α
let␈α
us␈α
construct␈α
a␈α
Lisp␈α
computation␈α
that␈α
does␈α
not␈α
terminate,␈α
but␈α
whose␈α
non-termination
␈↓ ↓H␈↓cannot␈α
be␈α
proved␈α
from␈α
the␈αaxioms␈α
Lisp1␈α
within␈α
first␈α
order␈αlogic.␈α
 We␈α
need␈α
only␈α
program␈αa␈α
proof-
␈↓ ↓H␈↓checker␈α
for␈αfirst␈α
order␈α
logic,␈αset␈α
it␈α
to␈αgenerate␈α
all␈αpossible␈α
proofs␈α
starting␈αwith␈α
the␈α
axioms␈αLisp1,
␈↓ ↓H␈↓and␈α
stop␈α
when␈α
it␈αfinds␈α
a␈α
proof␈α
of␈α(NIL␈α
≠␈α
NIL)␈α
or␈αsome␈α
other␈α
contradiction.␈α
 Assuming␈αthe␈α
axioms
␈↓ ↓H␈↓are␈α
consistent,␈αthe␈α
program␈αwill␈α
never␈α
find␈αsuch␈α
a␈αproof␈α
and␈α
will␈αnever␈α
stop.␈α In␈α
fact,␈αproving␈α
that
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *16


␈↓ ↓H␈↓the␈α⊂program␈α⊂will␈α⊂never␈α⊂stop␈α⊂is␈α⊃precisely␈α⊂proving␈α⊂that␈α⊂the␈α⊂axioms␈α⊂are␈α⊂consistent.␈α⊃ But␈α⊂G␈↓
:␈↓odel's
␈↓ ↓H␈↓theorem␈αasserts␈αthat␈αaxiom␈αsystems␈αlike␈αLisp1␈αcannot␈αbe␈αproved␈αconsistent␈αwithin␈αthemselves.␈α All
␈↓ ↓H␈↓the␈αknown␈αcases␈αof␈αterminating␈αcomputations␈αthat␈αcan't␈αbe␈αproved␈αnot␈αto␈αterminate␈αwithin␈αPeano
␈↓ ↓H␈↓arithmetic involve such an appeal to G␈↓
:␈↓odel's theorem or similar unsolvability arguments.

␈↓ ↓H␈↓␈↓ α_We␈α
can␈α
presumably␈α
prove␈α
Lisp1␈α
consistent␈α
just␈α
as␈α
Gentzen␈α
proved␈α
arithmetic␈α∞consistent␈α
-
␈↓ ↓H␈↓by␈α∩introducing␈α∪a␈α∩new␈α∩axiom␈α∪schema␈α∩that␈α∩allows␈α∪induction␈α∩up␈α∩to␈α∪the␈α∩transfinite␈α∪ordinal␈α∩ε␈↓β0␈↓.
␈↓ ↓H␈↓Proving the new system consistent would require induction up to a still higher ordinal, etc.

␈↓ ↓H␈↓␈↓ α_Since␈α∞every␈α∞recursively␈α∞defined␈α∞function␈α∞can␈α∞be␈α∞defined␈α∞explicitly,␈α∞any␈α∞sentence␈α
involving
␈↓ ↓H␈↓such␈αfunctions␈αcan␈αbe␈αreplaced␈αby␈αan␈αequivalent␈αsentence␈αinvolving␈αonly␈α␈↓↓occur␈↓␈αand␈αthe␈αbasic␈αLisp
␈↓ ↓H␈↓functions.␈α The␈αtheory␈αof␈α
␈↓↓occur␈↓␈αand␈αthese␈αfunctions␈αhas␈α
a␈αstandard␈αmodel,␈αthe␈αusual␈α
S-expressions
␈↓ ↓H␈↓and␈α∪many␈α∩non-standard␈α∪models.␈α∩ We␈α∪"construct"␈α∩non-standard␈α∪models␈α∩in␈α∪the␈α∩usual␈α∪way␈α∩by
␈↓ ↓H␈↓appealing␈α
to␈α
the␈α
theorem␈α
that␈α
if␈α
every␈α
finite␈α
subset␈α
of␈α
a␈α
set␈α
␈↓↓S␈↓␈α
of␈α
sentences␈α
of␈α
first␈α
order␈α
logic␈αhas␈α
a
␈↓ ↓H␈↓model,␈αthen␈α␈↓↓S␈↓␈αhas␈αa␈αmodel.␈α For␈αexample,␈αtake␈α␈↓↓S␈α=␈α{occur[␈↓NIL␈↓↓,␈αx],␈αoccur[␈↓(A)␈↓↓,␈αx],␈αoccur[␈↓(A␈αA)␈↓↓␈α,
␈↓ ↓H␈↓↓x],␈α...␈↓␈αindefinitely}.␈α Every␈αfinite␈αsubset␈αof␈α␈↓↓S␈↓␈αhas␈αa␈αmodel;␈αwe␈αneed␈αonly␈αtake␈α␈↓↓x␈↓␈αto␈αbe␈αthe␈αlongest
␈↓ ↓H␈↓list␈αof␈αA's␈αoccurring␈αin␈αthe␈αsentences.␈α Hence␈αthere␈αis␈αa␈αmodel␈αof␈αthe␈αLisp␈αaxioms␈αin␈αwhich␈α␈↓↓x␈↓␈αhas
␈↓ ↓H␈↓all␈α∞lists␈α∂of␈α∞A's␈α∞as␈α∂subexpressions.␈α∞ No␈α∞sentence␈α∂true␈α∞in␈α∞the␈α∂standard␈α∞model␈α∞and␈α∂false␈α∞in␈α∂such␈α∞a
␈↓ ↓H␈↓model␈αcan␈αbe␈αproved␈αfrom␈αthe␈αaxioms.␈α However,␈αit␈αis␈αnecessary␈αto␈αbe␈αcareful␈αabout␈αthe␈αmeaning
␈↓ ↓H␈↓of␈αtermination␈αof␈αa␈αfunction.␈α
 In␈αfact,␈αtaking␈αsuccessive␈α␈↓↓cdr␈↓s␈α
of␈αsuch␈αan␈α␈↓↓x␈↓␈αwould␈α
never␈αterminate,
␈↓ ↓H␈↓but␈α
the␈αsentence␈α
whose␈α␈↓↓standard␈α
interpretation␈↓␈αis␈α
termination␈αof␈α
the␈αcomputation␈α
is␈αprovable␈α
from
␈↓ ↓H␈↓Lisp1.

␈↓ ↓H␈↓␈↓ α_The␈α⊂practical␈α⊂question␈α∂is:␈α⊂where␈α⊂does␈α∂the␈α⊂correctness␈α⊂of␈α∂ordinary␈α⊂programs␈α⊂come␈α⊂in?␈α∂ It
␈↓ ↓H␈↓seems␈αlikely␈α
that␈αsuch␈α
statements␈αwill␈αbe␈α
provable␈αwith␈α
our␈αoriginal␈αsystem␈α
of␈αaxioms.␈α
 It␈αdoesn't
␈↓ ↓H␈↓follow␈α
that␈α
the␈α
system␈α
Lisp1␈α
will␈α∞permit␈α
convenient␈α
proofs,␈α
but␈α
probably␈α
it␈α
will.␈α∞ Some␈α
heuristic
␈↓ ↓H␈↓evidence␈α
for␈α
this␈α
comes␈α
from␈α
(Cohen␈α
1965).␈α
 Cohen␈α
presents␈α
two␈α
systems␈α
of␈α
axiomatized␈α
arithmetic
␈↓ ↓H␈↓Z1␈α
and␈α
Z2.␈α
 Z1␈α∞is␈α
ordinary␈α
Peano␈α
arithmetic␈α∞with␈α
an␈α
axiom␈α
schema␈α∞of␈α
induction,␈α
and␈α
Z2␈α∞is␈α
an
␈↓ ↓H␈↓axiomatization␈α
of␈αhereditarily␈α
finite␈α
sets␈αof␈α
integers.␈α Superficially,␈α
Z2␈α
is␈αmore␈α
powerful␈α
than␈αZ1,
␈↓ ↓H␈↓but␈αbecause␈αthe␈αset␈αoperations␈αof␈αZ2␈αcan␈αbe␈αrepresented␈αin␈αZ1␈αas␈αfunctions␈αon␈αthe␈αG␈↓
:␈↓odel␈αnumbers
␈↓ ↓H␈↓of␈α⊃the␈α⊃sets,␈α∩it␈α⊃turns␈α⊃out␈α∩that␈α⊃Z1␈α⊃is␈α⊃just␈α∩as␈α⊃powerful␈α⊃once␈α∩the␈α⊃necessary␈α⊃machinery␈α∩has␈α⊃been
␈↓ ↓H␈↓established.␈α Because␈αsets␈αand␈αlists␈αare␈αthe␈αbasic␈αdata␈αof␈αLisp1,␈αand␈αsets␈αare␈αeasily␈αrepresented,␈αthe
␈↓ ↓H␈↓power␈αof␈αLisp1␈αwill␈αbe␈αapproximately␈αthat␈αof␈αZ2,␈αand␈αconvenient␈αproofs␈αof␈αcorrectness␈αstatements
␈↓ ↓H␈↓should␈α
be␈αpossible.␈α
 Moreover,␈α
since␈αLisp1␈α
is␈αa␈α
first␈α
order␈αtheory,␈α
it␈α
is␈αeasily␈α
extended␈αwith␈α
axioms
␈↓ ↓H␈↓for␈α
sets,␈αand␈α
this␈α
should␈αhelp␈α
make␈α
informal␈αproofs␈α
easy␈αto␈α
express.␈α
 It␈αwould␈α
be␈α
nice␈αto␈α
be␈αable␈α
to
␈↓ ↓H␈↓express these considerations less vaguely.


␈↓ ↓H␈↓α10. References.

␈↓ ↓H␈↓␈↓αCartwright,␈αR.S.␈α(1977)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed
␈↓ ↓H␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.

␈↓ ↓H␈↓␈↓αCohen, Paul (1966)␈↓: ␈↓↓Set Theory and the Continuum Hypothesis␈↓, W.A. Benjamin Inc.

␈↓ ↓H␈↓␈↓αCooper,␈αD.C.␈α(1969)␈↓:␈α"Program␈αScheme␈αEquivalences␈αand␈αSecond-order␈αLogic",␈αin␈αB.␈αMeltzer␈αand
␈↓ ↓H␈↓D. Michie (eds.), ␈↓↓Machine Intelligence␈↓, Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.

␈↓ ↓H␈↓␈↓αKleene, S.C. (1951)␈↓: ␈↓↓Introduction to Metamathematics␈↓, Van Nostrand, New York.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *17


␈↓ ↓H␈↓␈↓αLuckham,␈αD.C.,␈αD.M.R.Park,␈α
and␈αM.S.␈αPaterson␈α(1970)␈↓:␈α
"On␈αFormalized␈αComputer␈αPrograms",␈α
␈↓↓J.
␈↓ ↓H␈↓↓CSS␈↓, ␈↓α4␈↓(3): 220-249 (June).

␈↓ ↓H␈↓␈↓αManna,␈αZohar␈αand␈α
Amir␈αPnueli␈α(1970)␈↓:␈α
"Formalization␈αof␈αthe␈α
Properties␈αof␈αFunctional␈α
Programs",
␈↓ ↓H␈↓␈↓↓J. ACM␈↓, ␈↓α17␈↓(3): 555-569.

␈↓ ↓H␈↓␈↓αManna, Zohar (1974)␈↓: ␈↓↓Mathematical Theory of Computation␈↓, McGraw-Hill.

␈↓ ↓H␈↓␈↓αManna,␈α∀Zohar,␈α∀Stephen␈α∀Ness␈α∀and␈α∀Jean␈α∀Vuillemin␈α∀(1973)␈↓:␈α∀"Inductive␈α∀Methods␈α∀for␈α∀Proving
␈↓ ↓H␈↓Properties of Programs", ␈↓↓Comm. ACM␈↓,␈↓α16␈↓(8): 491-502 (August).

␈↓ ↓H␈↓␈↓αMcCarthy,␈αJohn␈↓␈α(1963)␈α"A␈α
Basis␈αfor␈αa␈αMathematical␈αTheory␈α
of␈αComputation",␈αin␈αP.␈αBraffort␈α
and
␈↓ ↓H␈↓D.␈α⊃Hirschberg␈α⊃(eds.),␈α⊂␈↓↓Computer␈α⊃Programming␈α⊃and␈α⊂Formal␈α⊃Systems␈↓,␈α⊃pp.␈α⊃33-70.␈α⊂ North-Holland
␈↓ ↓H␈↓Publishing Company, Amsterdam.

␈↓ ↓H␈↓␈↓αMorris,␈α
James␈αH.,␈α
and␈αBen␈α
Wegbreit␈α
(1977)␈↓:␈α"Program␈α
Verification␈αby␈α
Subgoal␈αInduction",␈α
␈↓↓Comm.
␈↓ ↓H␈↓↓ACM␈↓,␈↓α20␈↓(4): 209-222 (April).

␈↓ ↓H␈↓␈↓αPark,␈α_David␈α_(1969)␈↓:␈α_Fixpoint␈α_Induction␈α_and␈α_Proofs␈α_of␈α_Program␈α_Properties",␈α_in␈α↔␈↓↓Machine
␈↓ ↓H␈↓↓Intelligence 5␈↓, pp. 59-78, Edinburgh University Press, Edinburgh.

␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Artificial Intelligence Laboratory
␈↓ ↓H␈↓Computer Science Department
␈↓ ↓H␈↓Stanford University
␈↓ ↓H␈↓Stanford, California 94305

␈↓ ↓H␈↓ARPANET: MCCARTHY@SU-AI